Program Correctness

In the first part of this course you will be introduced to the Hoare logic, which is a basic tool used to formally specify and verify the correctness of imperative programs. The second part shows a more refined version of Hoare logic to deal with Java-like OO programs.

You will need to download and print the following lecture notes:

  1. Introduction to a Correctness Approach in Programming
  2. List of Rules and Theorems
  3. Proof Outlines for Object-Oriented Programming

Course Plan (5 meetings)

Phase Topics Chapters Recommended exercises Assignment
PC-1,2 predicate logic, list induction LN1 chapters 1 - 4 Section 3.9: 1a,1b,2a,2b,*4,*7.
Section 4.3: 1a,1c,*2,*3a.
PC-2,3 basic Hoare logic for imperative programs LN1 chapters 5,6 Section 5.3: 1a,1b,1c,*4,5.
Section 6.11: *1,*2,*8,10,*11,14,*18,21,*22 		Assignment 1. Ignore the instruction about using SUBMIT.
PC-4,5 logic for OO LN-OO chapters 1-5 Exercises 2.1, *2.3, *3.1, *3.3, *4.1, *5.1 Assignment 2
. Ignore the instruction about using SUBMIT.
PC-6
program call LN1 chapter 7 Section 7.5: 1,2

Deliver your exercises in either PDF or plain ASCII format. Do NOT deliver a word document.

There is also a solution pack to help you do the exercises (see below).

Grading

You get 2 compulsory assignments (each weight equal) and 1 exam. The exam weights 50%. Your final grade of the PC-part is just the sum of every components, multiplied by their respective weight.

Supplementary Materials

Solution of the exercises in LN1: here.

Simple LaTeX style file to format your proof: here. Example: source + result.

Trial exam: 1 (leave out exercise 3 and 6 from Part II). And here is a (solution)