Lecture Log

Lecture 12: Specification and Verification

Title slideToday’s lecture was the first of three on language techniques and tools that aim to improve program correctness: not necessarily changing what a program does, the time or space it takes, or the power it uses; but making sure that what it does is the right thing to do. Of course, that also requires having some way to identify what that is to begin with.

Today’s lecture looked at the use of Hoare Logic for specifying desired behaviour, and a little about ways to confirm that a program meets a specification.

Link: Slides for Lecture 12 (no recording, sorry)

Homework

The lecture on Tuesday 8 November will be about some tools for checking Java programs, including ones that apply Hoare Logic and ideas of Design by Contract™ .

Read this: Before Tuesday, read this short article.

Do this: Find some information online about assertions in Java. Post a link to the Piazza group, with any comments you have on things you thought helpful or otherwise about what you found.

Optional extra: Slide 7 Hoare triples gives three example triples. Can you prove these using the derivation rules on Slide 11 Hoare rules? For any triples that in fact aren’t valid, can you fix them? Are they then derivable?

People

ACM Turing Award 1978 - Bob Floyd Robert (Bob) W Floyd
ACM Turing Award 1978
For having a clear influence on methodologies for the creation of efficient and reliable software, and for helping to found the following important subfields of computer science: the theory of parsing, the semantics of programming languages, automatic program verification, automatic program synthesis, and analysis of algorithms.
Link: ACM Turing Award Citation
ACM Turing Award 1980 - Tony Hoare C. Antony (Tony) R. Hoare
ACM Turing Award 1980
For his fundamental contributions to the definition and design of programming languages.
Link: ACM Turing Award Citation
Portrait of John Keats John Keats
Image © National Portrait Gallery, London
 
Ode on a Grecian Urn
Beauty is truth, truth beauty — that is all
Ye know on earth, and all ye need to know
 
Link: Oxford Book of English Verse

References

C. A. R. Hoare. An axiomatic basis for computer programming. Communications of the ACM 12(10):576–580, 1969. DOI 10.1145/363235.363259
Hoare’s original article setting out the use of triples. Note that this uses the notation P{C}Q with braces around the command rather than the assertions.
Hoare and Jones (editor), Essays in Computing Science. ACM Classic Books Series. Originally published by Prentice Hall, 1989.
A collection of articles by Hoare. Proving programs correct is addressed in most chapters, but particularly 4 and 5.
Eiffel Software. The Power of Design by Contract™.
Design methodologies often attract heated discussion of their effectiveness. For example, would design by contract have averted the Ariane disaster? Yes, we’re back to rocket science. Look at the following two articles:

Tobias Nipkow. Hoare Logics for Recursive Procedures and Unbounded Nondeterminism. In Computer Science Logic: Proceedings of CSL 2002. Springer, 2002. DOI: 10.1007/3-540-45793-3_8
Article describing a machine-checked proof that Hoare logic is sound and complete. Section 3 gives some history of the “consequence” rule. This is fairly technical, but I think well-written and with the first section giving a good overview of the history and issues here.