Specifying generic Java programs: two case studies

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 key features are the introduction of parametricity both for types and for theories and an instantiation relation between theories. We discuss soundness conditions and their verification.