Reasoning about Java programs in higher order logic using PVS and Isabelle

Abstract

This thesis describes the first steps of a project aimed at formal verification of Java programs. The work presented here is part of a larger project called LOOP, for Logic of Object Oriented Programming. A semantics for Java is described in type theory and it is shown how this semantics forms the basis for program verification. The verifications are done with the use of interactive theorem provers,namely PVS and Isabelle. Both theorem provers are described in some detail, resulting in a comparison of the strong and weak points of both systems. A Hoare logic is discussed, which is especially tailored to reasoning about Java. The LOOP project resulted in the construction of the so-called LOOP compiler, which takes Java classes as input and returns PVS or Isabelle theories, capturing the semantics of the Java program, as output. This thesis also briefly describes a specification language for Java, called JML (Java modeling language). This language can be used to specify Java classes.Finally, two non-trivial case studies are described in this thesis, verifying properties of standard Java library classes. The first case study verifies a class invariant over class Vector, the second case study verifies the functional behaviour of the class AbstractCollection