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:
|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||
. Ignore the instruction about using SUBMIT.
||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).
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)