Lecture 3: References

18 January 2010

Here are some pointers for recommended further reading and references from Lecture 3.

Read the rest of this entry »


Lecture 3: Hoare Logic

18 January 2010

First-order logic; 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 Thursday. 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!