Modular Specification of Java Programs

Theme : Programmation, verication et preuvesEquipes-Projets PROVAL et CASSISRapport de recherche n° 7097 — November 2009 — 26 pagesAbstract: This work investigates the question of modular specication of generic Java classes and methods. Therst part introduces a specication language for Java programs. In the second part the language is used to specifyan array sorting algorithm by selection. The third and the fourth parts dene a syntax proposal for the specicationa generic Java programs, through two examples. The former is the specication of the generic method for sortingarrays which comes in the java.util.Arrays class of the Java API. The latter is the specication of thejava.util.HashMap class and its use for memoization.Key-words: Formal Specication, Verication, Proof, Automated Reasoning, SMT Provers, Krakatoa ModelingLanguage