Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2001 | 10.1007/3-540-45314-8_21 | FASE |
Keywords | DocType | ISBN |
nijmegen jml,jml specification,java modeling language jml,specialised logic,jml annotation,java class,hoare logic,java modeling language,higher order logic,back-end theorem prover,java program,design by contract,theorem prover | Conference | 3-540-41863-6 |
Citations | PageRank | References |
53 | 4.76 | 16 |
Authors | ||
2 | ||