Paper Info

Title | ||
---|---|---|

A Logic for the Java Modeling Language JML |

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 |