Advances in Programming Languages 2010

Verification at different levels (design, specification, implementation) and horizontal/vertical translations (refinement, optimisation, compilation). Forms of certification and example approaches: proof-carrying code, translation validation and compiler correctness.

I mentioned some example research projects which have (hopefully!) working demos.

Links: Slides; research projects: MRG, Mobius, Compcert.

Homework

• Read more about the MRG project, and try to understand the demos. What happens when you adjust the various bits of PCC input?
• Prepare for next Monday’s lecture by reading the paper
  
  Interfaces and specifications for the Smalltalk-80 collection classes

ESC/Java2: a verification tool combining several analysis techniques (types, dataflow, proof). An overview of the checks it performs: exception freedom for common exceptions (null pointers, array indices, class casts). The lack of soundness and completeness: false positives and defects missed. Some further and specialised annotations extending core JML (non_null, unreachable, modifies, pure). Specification inheritance.

Links: Slides; ESC/Java2 downloads.

Homework

1. Try ESC/Java on some of the example files and some Java (1.4) programs of your own (see below how to run ESC/Java2 on DICE).
2. Try to statically verify your previously written recipe card program with ESC/Java2.

Read the rest of this entry »

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.

Links: Slides; JML.tar.gz download.

Homework

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.