Specifying Generic Java Programs: two case studies

Alain Giorgetti (1, 2) , Claude Marché (3, 4) , Elena Tushkanova (1, 2) , Olga Kouchnarenko (1, 2)

1 FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174)
2 CASSIS - Combination of approaches to the security of infinite states systems
3 LRI - Laboratoire de Recherche en Informatique
4 PROVAL - Proof of Programs

This work investigates the question of modular specification of generic Java classes and methods. We propose extensions to the Krakatoa Modeling Language, a part of the Why platform for proving that a Java or C program is a correct implementation of some specification. The new constructs we propose for the specification of generic Java programs are presented through two significant examples: the specification of the generic method for sorting arrays which comes from the java.util.Arrays class in the Java API, and the specification of the java.util.HashMap class defining a generic hash map and its use for memoization. The main ingredient is the notion of theories and the instantiation relation between them. We discuss soundness conditions and their verification.

Domaines: Logique en informatique [cs.LO]

Alain Giorgetti, Claude Marché, Elena Tushkanova, Olga Kouchnarenko. Specifying Generic Java Programs: two case studies. 11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010, Mar 2010, Paphos, Cyprus. pp.92--106. ⟨inria-00525784⟩