Review of Hoare logic. Model-based specification as a technique for system design. Design features of JML. Some examples: preconditions, postconditions, invariants; model variables, methods and classes; ghost variables, assertions, assumptions. JML as a common language across multiple tools for software specification and verification.
Lecture 7: JML – the Java Modeling Language
2 February 2009
Comments Off on Lecture 7: JML – the Java Modeling Language | 
Lecture log | 
Permalink
Posted by David Aspinall
