Reasoning about Java classes

Computing Science Institute, University of Nijmegen

This talks presents the first results of a project called LOOP, on formal methods for the object-oriented language Java. It aims at verification of program properties, with support of modern tools. We use our own front-end tool (which is still partly under construction) for translating Java classes into higher order logic, and a back-end theorem prover (namely PVS, developed at SRI) for reasoning.

This is a big topic, and we shall concentrate on the following 2 aspects.

A state transformer semantics for Java statements and expression will be described in the higher-order logic of PVS, including non-termination, normal termination and abrupt termination, e.g. because of an exception, break, return or continue.

With this semantics, properties about non-looping Java programs can be proven directly, by automatic rewriting using the definitions. However, to reason about e.g. while loops, more sophisticated methods have to be used. To this end, Hoare logic rules are mechanically derived with respect to this semantics. These rules deviate from the traditional Hoare logic rules, in that they enable reasoning about programs which may contain exceptions, breaks, continues and returns.

As a case study, a class invariant of class Vector is proven correct in PVS. This class invariant essentially says that the number of elements in a vector never exceeds its capacity. In this verification, our Hoare logic rules turned out to be very useful.

For more information on the LOOP project, see: http://www.cs.kun.nl/~bart/PAPERS/OOPSLA98.ps.Z

LS Home page or Talks in 1998/99