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 Lorraine, LORIA - Laboratoire Lorrain de Recherche en Informatique et ses Applications
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.
Type de document :
Communication dans un congrès
11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010, Mar 2010, Paphos, Cyprus. pp.92--106, 2010
Liste complète des métadonnées

Littérature citée [14 références]  Voir  Masquer  Télécharger

https://hal.inria.fr/inria-00525784
Contributeur : Alain Giorgetti <>
Soumis le : mardi 12 octobre 2010 - 17:08:52
Dernière modification le : vendredi 6 juillet 2018 - 15:06:10
Document(s) archivé(s) le : jeudi 13 janvier 2011 - 02:53:49

Fichier

gmtkLDTA2010.pdf
Fichiers produits par l'(les) auteur(s)

Identifiants

  • HAL Id : inria-00525784, version 1

Citation

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, 2010. 〈inria-00525784〉

Partager

Métriques

Consultations de la notice

392

Téléchargements de fichiers

219