Verification of java’s abstractcollection class: A case study

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

9 Citations (Scopus)


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.
Original languageEnglish
Title of host publicationMathematics of Program Construction
Subtitle of host publication6th International Conference, MPC 2002 Dagstuhl Castle, Germany, July 8–10, 2002 Proceedings
EditorsEerke A. Boiten, Bernhard Möller
Place of PublicationBerlin, Heidelberg
ISBN (Electronic)978-3-540-45442-7
ISBN (Print)978-3-540-43857-1
Publication statusPublished - 2002
Externally publishedYes
Event6th International Conference on Mathematics of Program Construction, MPC 2002 - Dagstuhl Castle, Germany
Duration: 8 Jul 200210 Jul 2002
Conference number: 6

Publication series

NameLecture Notes in Computer Science
ISSN (Print)0302-9743


Conference6th International Conference on Mathematics of Program Construction, MPC 2002
Abbreviated titleMPC
CityDagstuhl Castle


  • Java program
  • Proof obligation
  • Java modeling language
  • Loop body
  • Hoare logic


Dive into the research topics of 'Verification of java’s abstractcollection class: A case study'. Together they form a unique fingerprint.

Cite this