Description

Homework 6: Loop Bounds and Array Assignments
Prof. Stefan Muller
Updated Nov. 10
This assignment contains 5 written task(s) for a total of 70 points, in addition to a maximum of 0 bonus 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 Loop Bounds and Proof Outlines
Task 1.1 (Written, 16 points).
Updated 11/10: The task that was here before was way more difficult than we intended (and actually impossible as written). Please do this task instead.
In class, we said that a loop bound was like filling your car with gas and driving: as you drive, the amount of gas in your tank always decreases and when it reaches 0, you can’t drive any more. But hybrid cars make this more complicated: sometimes they don’t use gas at all, they just use the battery to drive; at other times, they use a little more gas to drive and also charge the battery. This is simulated by the following program. We can’t just use gas as a bound expression, because it doesn’t always decrease. But we can still find a bound expression.
Fill the blanks of the following the minimal proof outline, and convert it to a full proof outline. Remember you need to prove termination as well as partial correctness.
[gas0 = gas ∧ gas > 0 ∧ batt = 0]
miles := 0;
{inv∧ gas ≥ 0 ∧ batt ≥ 0}
{dec}
while (gas > 1 ∨ batt > 0) do if
else
gas := gas − 2; batt := batt + 1
fi
miles := miles + 1; od
[miles ≥ gas0 − 1]
Task 1.2 (Written, 12 points).
Fill the blanks to complete the following minimal proof outline by adding a loop invariant and bound expression to each while loop (note they are nested!). You do not need to convert it to a full proof outline. For each bound expression, explain in 1-2 sentences:
1. Why the loop invariant of the same loop implies the bound expression is always nonnegative.
2. How you know the bound expression decreases each loop iteration.
[∀i ∈ Z.(0 ≤ i < |a|) → a[i] ≥ 0]
i := 0;

i := i + 1
od [∀i ∈ Z.(0 ≤ i < |a|) → a[i] = 0]
Task 1.3 (Written, 12 points).
Assume that t is a valid bound expression, i is a variable and k is a constant. For each of the following, say whether it’s a valid bound expression or not, and explain in 1-2 sentences.
√
a) t
b) t2
c) t + i
d) t + i2
e) t + k
f) t + k2
2 Weakest Preconditions with Array Assignments
Task 2.1 (Written, 30 points).
Calculate the following weakest liberal preconditions and weakest preconditons (make sure to note which we are asking for!). Show your work, and simplify the expression as much as possible.
a) wlp(a[if x = 0 then i else j] := 1,a[i] = 1)
b) wlp(a[i] := 5,a[a[1]] = 5)

c) wlp(a[j] := a[i] + 1,a[j] > a[i])
d) wlp(i := 5;a[i] := a[i + 1],a[i] > 0)
e) wp(i := 5;a[i] := a[i + 1],a[i] > 0)
f) wlp(if i = j then j := j + 1 else a[j] := a[i] + 1 fi,a[j] > a[i])
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.