Java Program Verification at Nijmegen: Developments and Perspective
Bart Jacobs, Erik Poll · Radboud Repository (Radboud University) · 2004
A b str a c t.This paper presents a historical overview of th e work on Java program verification a t th e U niversity of Nijmegen (the N etherlands) over th e past six years (1997)(1998)(1999)(2000)(2001)(2002)(2003).It describes th e developm ent an d use of th e LO O P tool th a t is central in th is work.Also, it gives a perspective on th e field. In tro d u ctio nT he L O O P p ro ject sta rte d o u t as an exploration of th e sem antics of objectoriented languages in general, and Java in p articu lar.It has evolved to becom e w hat we believe is one of th e largest a tte m p ts to d ate at form alising a real program m ing and using th is form alisation as a basis for program verification.It is p ro b ab ly also one of th e largest a tte m p ts to d ate a t using m echanical theorem provers.T his p ap er a tte m p ts to give an overview of th e whole project.It is unavoidable th a t we have to resort to a high level of ab stra ctio n to do th is in th e lim ited space here.T herefore, our m ain aim is to convey th e general principles and we will frequently refer to o ther p apers for m uch m ore of th e technical details.From th e o u tset, a goal of th e p ro ject has been to reason a b o u t a real pro gram m ing language, an d n o t ju s t a toy object-oriented language.A p art from leaving o u t th re a d s, all th e com plications of real Java are covered, incl.-side-effects in expressions (som ething often om itted in th e to y languages stu d ied in th eo retical com puter science), -exceptions an d all o th er forms of a b ru p t control flow (including th e m ore b aroque co n stru cts th a t Java offers, such as labelled breaks and continues), -sta tic an d n o n -static field and m ethods, -overloading, -all th e com plications of Ja v a 's inheritance m echanism , including la te binding for m ethods, early binding for fields, overriding of m ethods, and shadow ing (or hiding) of fields.A p art from th re a d s, th e only m ajo r feature of Jav a no t su p p o rted is inner classes.T h e L O O P t o o l W h a t we call th e L O O P tool is effectively a com piler, w ritten in O 'Cam l.Fig. 1 illu strates roughly how it is used.As in p u t, th e L O O P tool takes sequential Jav a program s, and specifications w ritte n (as an n o tatio n s in th e Jav a source files) in th e Java M odeling Language JM L [24].Fig. 2 gives an exam ple of a Jav a class w ith a JM L specification.As o u tp u t, th e L O O P tool generates several files which, in th e sy n tax of th e theorem prover PV S [31], describe th e m eaning of th e Java program and its JM L specification.T hese files can be loaded into PV S, and th e n one can try to prove th a t th e Java program m eets its JM L specification.In ad d itio n to th e au to m atically generated PV S files, th ere are also several h a n d -w ritte n PV S files, th e so-called prelude.These files define th e basic building blocks for th e Jav a an d JM L sem antics, and define all th e m achinery needed, in th e form of PV S theories and lem m as, to su p p o rt th e actual work of program verification.interaction A .ja v a Java program m + JM L specification LO O P compiler A.pvs denotation [m] + proof obligations PVS theorem prover QED F ig. 1. T he L O O P tool as pre-processor for PVS userO r g a n is a tio n o f t h is p a p e r T he n ex t section begins by giving an exam ple of a Jav a p rogram w ith JM L specification to illu stra te th e kind of program verifi cation we are doing.T h e organisation of th e rest of th is p ap er is th e n m ore or less chronological, an d follows th e b o tto m -u p approach th a t we have tak en over th e years, sta rtin g a t th e detailed rep resentation of th e Jav a sem antics a t a low level, on to p of which fu rth er abstractio n s are built.T he L O O P project sta rte d w ith definition of a form al sem antics for Jav a in higher-order logic, by giving a so-called shallow em bedding, and using coalgebras as a m eans of organising th e sem antics of objects.T his is described in Sect.3. T he pro ject th e n evolved to also provide a form al sem antics of th e Jav a specification language JM L in PV S, as discussed in Sect.4, and to provide techniques for th e verification Java program s w ith JM L specifications on th e basis of these form al sem antics, which we discuss in Sect. 5. Sect.6 com pares th e L O O P p rojects w ith o th er work on providing theo rem prover su p p o rted program verification for Java.