inria-00525784, version 1
Specifying Generic Java Programs: two case studies
Alain Giorgetti a, 1, 2Claude Marché b, 3, 4Elena Tushkanova a, 1, 2Olga Kouchnarenko a, 1, 2
11th International Workshop on Language Descriptions, Tools, and Applications - LDTA'2010 (2010) 92--106
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.
- a – Université de Franche-Comté
- b – Université de Paris-Sud Orsay
- 1: Laboratoire d'Informatique de Franche-Comté (LIFC)
- Université de Franche-Comté : EA4269
- 2: CASSIS (INRIA Lorraine - LORIA / LIFC)
- INRIA – CNRS : UMR7503 – CNRS : FRE2661 – Université de Franche-Comté – Université Henri Poincaré - Nancy I – Université Nancy II – Institut National Polytechnique de Lorraine (INPL)
- 3: Laboratoire de Recherche en Informatique (LRI)
- CNRS : UMR8623 – Université Paris XI - Paris Sud
- 4: PROVAL (INRIA Saclay - Ile de France)
- INRIA – Université Paris XI - Paris Sud – CNRS : UMR
- Domain : Computer Science/Logic in Computer Science
- inria-00525784, version 1
- http://hal.inria.fr/inria-00525784
- oai:hal.inria.fr:inria-00525784
- From: Alain Giorgetti
- Submitted on: Tuesday, 12 October 2010 17:08:52
- Updated on: Monday, 18 October 2010 14:03:14
Associated documents
Export