Abstract.
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.
Article PDF
Similar content being viewed by others
Avoid common mistakes on your manuscript.
Author information
Authors and Affiliations
Additional information
Published online: 10 May 2001
Rights and permissions
About this article
Cite this article
Huisman, M., Jacobs, B. & van den Berg, J. A case study in class library verification: Java’s vector class. STTT 3, 332–352 (2001). https://doi.org/10.1007/s100090100047
Issue Date:
DOI: https://doi.org/10.1007/s100090100047