Reasoning about Java

A next step in the development of the LOOP tool is the translation of Java classes. The aim is to enable reasoning about classes in Java for verification purposes---and not meta-level reasoning about Java as a programming language. Roughly, the LOOP tool translates these Java classes to an internal format which is very similar to the one used for CCSL classes: the fields and methods are translated into coalgebraic operations, and the method body definitions are translated into assertions relating the methods to their bodies. The fields and methods become functions acting on a state space. This corresponds to the fact that they have an implicit argument this in Java (and in other object-oriented languages).

As an example, we consider the coalgebraic representation of expressions, say of type int, as resulting for example from a Java method declaration: 

   int size() { ... }
Such a method has three possible output options: These three options are captured by representing such expressions as coalgebras of the form: 
  Self -----> 
     {hang} + (Self x int) + (Self x RefType)
where + is disjoint union, x is cartesian product, and RefType is a special type used for reference (to exceptions in this case). Typically for coalgebras, such a function has a domain type consisting of only the state space Self, and a codomain type which has more structure.

Statements (producing void) are represented similarly. On the basis of this representation all language constructs of Java (without threads), like while or try {...} catch(...) { ... }, are defined (in PVS and in Isabelle/HOL). This forms the basis for the actual verifications.

The first paper describing the LOOP tool on Java classes is [JacobsEtAl:OOPSLA98]. Details about the representation of Java statements, expressions and language constructs are available from [HuismanJ:FASE00], together with an extension of Hoare logic developed specifically for this semantics. Information about the underlying object memory model can be obtained from [BergEtAl:WADT99], about inheritance from [HuismanJ:TPHOL00], and about exceptions from [Jacobs:ESOP01]. An alternative, monadic description (instead of coalgebraic ) of the semantics is in [JacobsP:AMAST00]. A non-trivial application is the verification of an invariant property for the Vector class from the standard Java API, see [ HuismanEtAl:FTfJP99].