|
M. Huisman, Bart Jacobs, J. van den Berg, A case study in class library verification: Java's vector class. Software Tools for Technology Transfer 3(3), 2001, p.332-352.
This paper presents a verification of an invariant property for the Vector class from Java's standard library (API). The property says (essentially) that the actual size of a vector is less than or equal to its capacity. It is shown that this "safety'' or "data integrity'' property is maintained by all methods of the Vector class, and that it holds for all objects created by the constructors of the Vector class. The verification of the Vector class invariant is done with the proof tool PVS. It is based on a semantics of Java in higher order logic. The latter is incorporated in a special purpose compiler, the LOOP tool, which translates Java classes into logical theories. It has been applied to the Vector class for this case study. The actual verification takes into account the object-oriented character of Java: (non-final) methods may always be overridden, so that one cannot rely on a particular implementation. Instead, one has to reason from method specifications in such cases. This project demonstrates the feasibility of tool-assisted verification of non-trivial properties for non-trivial Java classes.
Not overly exciting, but a useful example none the less.
The paper shows that real class libraries can be verified using well known techniques, coupled with automatic tools. The Java Modeling Language (JML) is used for behavioural specification.
One interesting aspect of this work is the explicit reasoning regarding abrupt termination (e.g., exceptions).
Posted to theory by Ehud Lamm on 11/1/03; 11:27:29 PM
|
|
A case study in class library verification: Java's vector class
