Description

Homework 4: WP and SP
Prof. Stefan Muller
This assignment contains 5 task(s) for a total of 28 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.
Read the policy on the website and be sure you understand it.
1
1 Weakest Preconditions
Compute the following using the algorithms given in class. Show the steps you take to get to your answer. You don’t need to simplify the conditions. Task 1.1 (Written, 12 points).
a) (3 points) wlp(n := sqrt(y) +1;n := x ∗ n;skip,n = 0)
b) (3 points) wp(n := sqrt(y) + 1;n := x ∗ n;skip,n = 0)

c) (6 points) wp(y := −1;if y > 0 then z := 1 else z := x/y fi,z = 1)
Task 1.2 (Written, 5 points).
Consider a program S and a condition P. What is the relation between P and wlp(S,sp(S,P))? In particular, do we have wlp(S,sp(S,P)) ⇒ P? If yes, provide a proof, if not a counterexample.
2 Strongest Postconditions
Task 2.1 (Written, 6 points).
Compute the following using the algorithms given in class. Show the steps you take to get to your answer. You don’t need to simplify the conditions.
a) (3 points) sp(x := −1;if y > 0 then x := 1 else z := x/y fi,y ≥ 0)
b) (3 points) sp(if y = 0 then x := x ∗ 5 else skip fi,x = 10)
Task 2.2 (Written, 5 points).
Consider a program S and a condition Q. What is the relation between the postcondition Q and sp(S,wlp(S,Q))? In particular, do we have sp(S,wlp(S,Q)) ⇒ Q? If yes, provide a proof, if not a counterexample.
3 One more wrap-up question
Task 3.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.
2