Description

Homework 3: Hoare triples and proofs
Prof. Stefan Muller
This assignment contains 10 written task(s) for a total of 77 points.
Logistics
Please read and follow these instructions carefully.
• Submit your written answers in a single PDF or Word document. Typed answers are preferred (You can use any program as long as you can export a .pdf, .doc or .docx; LaTeX is especially good for typesetting logic and math, and well worth the time to learn it), but legible handwritten and scanned answers are acceptable as well.
• Your Blackboard submission should contain only the file with your written answers. Do not compress or put any files in folders.
This homework is to be completed individually. Read the policy on the website and be sure you understand it.
1 Hoare triples
Task 1.1 (Written, 10 points).
Let s = while i < x do x := x ∗ i;i := i + 1 od. For each of the following, is the triple satisfied or unsatisfied in the given state? Explain why by unfolding the definition as we saw in the class. Note that some of these are partial correctness triples and others are total correctness.
a) {i = 1,x = 6}⊨ [ i < x ] s [ i = x ]
b) {i = −1,x = 5}⊨{i < x} s {i ≥ 0 ∧ x ≤ 0}
c) {i = 1,x = 0}⊨{i < x} s {i = x}
d) {i = 1,x = 2}⊨{x = k} s {x = k!}
e) {i = 1,x = 6}⊨{T} s {∃k.x = k!}
Task 1.2 (Written, 6 points).
Consider program s in the previous task. For each of the following triples, say if it’s valid (satisfied in all states or not). If not, provide a counterexample and then fix either the precondition, or the postcondition or the statement to make the triple valid. Don’t make your change trivial (that is, don’t make the precondition a contradiction, the postcondition a tautology or the statement soemthing that always errors or diverges).
a) {T} s {x > 0}
b) {x = k} s {x = k}
c) [ i = 1 ∧ x = k ∧ x > 0 ] s [ i = k ∧ x = k! ]
Task 1.3 (Written, 5 points).
Fill in an appropriate precondition such that the following triple is valid. Don’t provide a trivial precondition (that is, don’t make the precondition a contradiction).
[ ] n := −m;while n ̸= 0 do r := r ∗−3;n := n − 1 od [ r = 3m ]
Task 1.4 (Written, 3 points).
Write a precondition P1 such that the triple ⊨ [P1]x := sqrt(x)/y [T] is valid. Don’t make your precondition trivial (a contradiction). Explain by unfolding the definition of the triple as we saw in the class.
Task 1.5 (Written, 8 points).
a) Write a program S2 and a precondition P2 such that ̸⊨ [P2]S2[T]. Explain by unfolding the definition of the triple as we saw in the class.
b) Have you used a while clause in S2? If yes, can you provide another S2 this time without using the while clause? If no, can you provide another S2 this time with using the while clause?
Task 1.6 (Written, 8 points).
a) Write a triple for the following program that is valid if and only if the program terminates when the initial value of x is greater than three.
while x > 1 do if even(x) then x := 5x + 1 else x := x/2 fi od
b) Write another triple for the above program which is valid if and only if the program does not terminate when the initial value of x is less than or equal to three.
2 Substitution
Task 2.1 (Written, 10 points).
a) [y + 2/y]∃z.∀x.(x + y ≥ z + y)
b) [y + 2/x]∃z.∀x.(x + y ≥ z + y)
c) [x + 2/y]∃z.∀x.(x + y ≥ z + y)
d) [z/x](x ≥ z → (∃z.∀x.x + y ≥ z + y) ∧ y > z)
s := x − 2 {s ≥ 0 ∧ s%3 = 0}⇒{s%3 = 0}
fi {s%3 = 0}
fi {s%3 = 0}
e) [z/x](x ≥ z → (∃x.x + y ≥ z + y) ∧ y > z)
3 Proofs and Proof Outlines
Task 3.1 (Written, 20 points).
a) Write a program in IMP that given an array a of size two, returns its maximum element in variable m.
b) Write a partial correctness triple to state that your program does what is described in part (a).
c) Prove your partial correctness triple in Hoare logic using either proof trees or Hilbert-stlye proofs.
d) Write a proof outline for your partial correctness triple. You can use either rule for if that we discussed in class.
Task 3.2 (Written, 7 points).
Convert the following proof outline to a Hilbert-style proof. The remainder operator x%y returns the remainder when x is divided by y.
{x ≥ 0}

if(x%3 = 0) then {x ≥ 0 ∧ x%3 = 0}
s := x {s ≥ 0 ∧ s%3 = 0}⇒{s%3 = 0}
else {x ≥ 0 ∧ x%3 ̸= 0}
if(x%3 = 1) then {x ≥ 0 ∧ x%3 ̸= 0 ∧ x%3 = 1}⇒{x − 1 ≥ 0 ∧ x − 1%3 = 0} s := x − 1 {s ≥ 0 ∧ s%3 = 0}⇒{s%3 = 0} else{x ≥ 0 ∧ x%3 ̸= 0 ∧ x%3 ̸= 1}⇒{x − 2 ≥ 0 ∧ x − 2%3 = 0}
4 One more wrap-up question
Task 4.1 (Written, 0 points).
How long (approximately) did you spend on this homework, in total hours of actual working time? Your honest feedback will help us with future homeworks.