This paper presents the specification and (modular) verification of Java’s AbstractCollection class. This work is done as a case study within the LOOP project (at the university of Nijmegen). It is the first major verification within the project using the theorem prover Isabelle. The class AbstractCollection is automatically translated into a series of Isabelle theories. The specifications, written in the Java Modeling Language (JML), give rise to appropriate proof obligations. The paper explains how the specifications are constructed and verified. When working on this case study, it became clear that there is a problem that is not documented in the informal documentation: when a collection contains a reference to itself it has unexpected behaviour. It is discussed how the specifications are adapted to overcome this problem.
CITATION STYLE
Huisman, M. (2002). Verification of java’s abstractcollection class: A case study. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2386, pp. 175–194). Springer Verlag. https://doi.org/10.1007/3-540-45442-X_11
Mendeley helps you to discover research relevant for your work.