Details

Autor(en) / Beteiligte

• Jacobs, Bart
• Poll, Erik
• Hussmann, Heinrich

Titel

A Logic for the Java Modeling Language JML

Ist Teil von

• Fundamental Approaches to Software Engineering, 2001, p.284-299

Ort / Verlag

Berlin, Heidelberg: Springer Berlin Heidelberg

Erscheinungsjahr

2001

Quelle

Alma/SFX Local Collection

Beschreibungen/Notizen

• This paper describes a specialised logic for proving specifications in the Java Modeling Language (JML). JML is an interface specification language for Java. It allows assertions like invariants, constraints, pre- and post-conditions, and modifiable clauses as annotations to Java classes, in a design-by-contract style. Within the LOOP project at the University of Nijmegen JML is used for specification and verification of Java programs. A special compiler has been developed which translates Java classes together with their JML annotations into logical theories for a theorem prover (PVS or Isabelle). The logic for JML that will be described here consists of tailor-made proof rules in the higher order logic of the back-end theorem prover for verifying translated JML specifications. The rules efficiently combine partial and total correctness (like in Hoare logic) for all possible termination modes in Java, in a single correctness formula.