Topics
In our previous lecture, I attempted to give
you the flavour of the process of program verification. More
precisely, I offered an informal introduction to partial and total
correctness of programs, and to the proof rules that can be used
to establish partial correctness assertions for the statements in the
language While.
The informal proof rules that we discovered, and used to establish
partial correctness assertions for some simple programs, form the
basis for the more formal treatment we shall offer in the first part
of today's lecture. More precisely, we shall develop a proof system
for partial correctness assertions, and briefly examine its two key
properties, viz.
- Soundness, i.e., every partial correctness assertion that is provable is valid, and
- Completeness, i.e., every valid partial correctness assertion can be proven.
We shall finish the course with a revision session on syntax and semantics
(driven by your questions), and with the ritual examination of the
syllabus for the exam, and the list of exam questions.