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.
First: please do the homework from Lecture 3! Then I can show solutions and give help in the next lecture.
Next: you must try out JML in practice by downloading and running some of the suggested tools. Try the recipe card specification homework described on the last slide from Lecture 4. It should be fun!
I recommend starting from the JML.tar.gz download described at the bottom of the JML download page. It has pre-compiled tools for several platforms. You will need a Java 1.4 runtime as well (later versions may cause difficulties). If your operating system doesn’t come with one start from Sun’s product archive.