Skip to Main content Skip to Navigation
Conference papers

Specifying Generic Java Programs: two case studies

Alain Giorgetti 1, 2 Claude Marché 3, 4 Elena Tushkanova 1, 2 Olga Kouchnarenko 1, 2
2 CASSIS - Combination of approaches to the security of infinite states systems
FEMTO-ST - Franche-Comté Électronique Mécanique, Thermique et Optique - Sciences et Technologies (UMR 6174), Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
4 PROVAL - Proof of Programs
UP11 - Université Paris-Sud - Paris 11, Inria Saclay - Ile de France, CNRS - Centre National de la Recherche Scientifique : UMR
Abstract : 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.
Document type :
Conference papers
Complete list of metadata

Cited literature [14 references]  Display  Hide  Download
Contributor : Alain Giorgetti Connect in order to contact the contributor
Submitted on : Tuesday, October 12, 2010 - 5:08:52 PM
Last modification on : Friday, January 21, 2022 - 3:09:01 AM
Long-term archiving on: : Thursday, January 13, 2011 - 2:53:49 AM


Files produced by the author(s)


  • HAL Id : inria-00525784, version 1


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⟩



Les métriques sont temporairement indisponibles