Abstract
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 language | English |
|---|---|
| Title of host publication | Mathematics of Program Construction |
| Subtitle of host publication | 6th International Conference, MPC 2002 Dagstuhl Castle, Germany, July 8–10, 2002 Proceedings |
| Editors | Eerke A. Boiten, Bernhard Möller |
| Place of Publication | Berlin, Heidelberg |
| Publisher | Springer |
| Pages | 175-194 |
| ISBN (Electronic) | 978-3-540-45442-7 |
| ISBN (Print) | 978-3-540-43857-1 |
| DOIs | |
| Publication status | Published - 2002 |
| Externally published | Yes |
| Event | 6th International Conference on Mathematics of Program Construction, MPC 2002 - Dagstuhl Castle, Germany Duration: 8 Jul 2002 → 10 Jul 2002 Conference number: 6 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer |
| Volume | 2386 |
| ISSN (Print) | 0302-9743 |
Conference
| Conference | 6th International Conference on Mathematics of Program Construction, MPC 2002 |
|---|---|
| Abbreviated title | MPC |
| Country/Territory | Germany |
| City | Dagstuhl Castle |
| Period | 8/07/02 → 10/07/02 |
Keywords
- Java program
- Proof obligation
- Java modeling language
- Loop body
- Hoare logic