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


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!

Lecture 2: Coursework assignment topics

14 January 2010

Homework followup: closures in different languages; how C function pointers are not closures; feature interaction and closure oddity in Javascript.

Presentation of coursework topics; suggested report outline; notes on working practices.

Links: Slides; Coursework assignment; Function pointers in C are not closures: f1 f2 f3 f4.

LFCS Seminar

13 January 2010

Programming Language Ideas Escape the Lab: A Declarative Data Description Language for Managing Ad Hoc Data

Kathleen Fisher
AT&T Labs Research
4pm Thursday, 14th January, 2009
Room 4.31/33, Informatics Forum

Links: Seminar abstract; LFCS Seminar series

This talk describes the PADS data description language, which allows existing ad-hoc data to be processed into well-behaved standardised formats like XML. There are even machine learning algorithms to automatically infer appropriate PADS descriptions from a body of sample data. The work described is based on a range of advances in the theory of programming languages and machine learning.

Kathleen Fisher is an excellent speaker, visiting Edinburgh from the US, and I recommend this seminar for those interested in the APL course.

You may need to sign in to enter the Forum, but state that you are attending a research seminar, following item 3 of the Forum access policy.

Another room change

13 January 2010

From this Thursday lectures will be in AT2.11, not AT2.14. This is still in the Appleton Tower, on the same floor, but down at the end of the corridor. The room is smaller, but the seats (a) have desks in front and (b) do line up with the screen.

Lecture 1: References

11 January 2010

The references for lectures can get rather lengthy, so I’m putting them in a separate posting.  This time we have a list of sources for the various quotes in the lecture.  Comments, corrections, and additional material welcome.

Read the rest of this entry »