Lecture 13: Assertions and Hoare Logic

9 November 2010

Runtime assertions in Java with the assert statement. Logical assertions in Hoare Logic, building on first-order logic and a simple imperative language; Hoare triples. Rules for derivation; validity with respect to an operational semantics; soundness and completeness. Applications in program specification and verification; tools for formal verification; Design by Contractâ„¢ and lightweight verification.

Link: Slides

Homework

The next lecture is at 9am on Friday. Before then:

  1. Read the two JML articles mentioned in the lecture:
    1. Design by Contract with JML.
    2. An overview of JML tools and applications.
  2. Try to prove some of the example triples given in the slides using the Hoare rules and logic. This may be more intricate than you expect!
  3. Here are another couple of little exercises:
    1. Define a command C that computes the exponentiation function exp(m,n) and places the result in variable p. Give a correctness specification for it as a Hoare triple, and prove that C meets the specification.
    2. Devise a proof rule for an alternative loop command of the form do C while B .
  4. (For the techies): Try to install some of the JML tools, such as ESC/Java 2 (from Kind Software at the University of Dublin). If you succeed, please post details of what you did and some example test cases to prove it works. This is also more intricate than you might expect — installing research prototypes is sometimes a challenge. I am trying it too!