CSSE3100/7100 Reasoning about Programs
Week 2 Exercises
Exercise 2.1.
Determine how the following pairs of predicates are related, that is, which of the predicates is the weakest or strongest or if they are equivalent or if they are unrelated.
a) x <= 0 and x <= 1
b) x > 0 && y > 0 and x > 0
c) x > 0 || y >0 and x > 0
d) x >= 0 and x*x + y*y == 9
e) x >= 1 ==> x >= 0 and x >= 1
f ) (exists i :: i >= 0 && x == i ) and x >= 1
g) (exists i :: P && Q) and (forall i :: P ==> Q)
Exercise 2.2.
For each of the following triples, find initial values of x and y that demonstrate that the triple does not hold.
a) {true} x := 2*y {y <= x}
b) {x == 3} x := x + 1 {y == 4}
c) {true} x := 100 {false}
d) {x >= 0} x := x - 1 {x >= 0}
Exercise 2.3.
Compute the weakest precondition of the following statements with respect to the postcondition x + y < 100.
a) x := 32; y := 40
b) x := x + 2; y := y - 3*x
c) x, y := x + 2, y - 3*x
Exercise 2.4.
Verify that the following program correctly swaps x and y, where ^ denotes bitwise xor.
x := x ^ y;
y := x ^ y;
x := x ^ y;
Recall that the bitwise xor of a number with itself is 0, i.e., x ^ x = 0, and the bitwise xor of a number with zero is the number, i.e., x ^ 0 = 0 ^ x = x.
Exercise 2.5.
Suppose you want x + y == 22 to hold after the statement
if x < 20 { y := 3; } else { y := 2; }
then in which states can you start the statement? In other words, compute the weakest precondition of the statement with respect to x + y == 22. Simplify the condition after you have computed it.
Exercise 2.6.
Compute the weakest precondition for the following statement with respect to y < 10.
Simplify the condition.
if x < 8 {
if x == 5 {
y := 10;
} else {
y := 2;
}
} else {
y := 0;
}
Exercise 2.7.
Compute the weakest precondition for the following statement with respect to y % 2 == 0 (that is, "y is even"). Simplify the condition.
if x < 10 {
if x < 20 { y := 1; } else { y := 2; }
} else {
y := 4;
}
Exercise 2.8.
Determine under which circumstances the following program establishes 0 <= y < 100. If you're starting to get a hang of how to compute weakest preconditions, try to do the computation in your head. Write down the answer you come up with, and then write out the full wp reasoning to check that you got the right answer.
if x < 34 {
if x == 2 { y := x + 1; } else { y := 233; }
} else {
if x < 55 { y := 21; } else { y := 144; }
}
Exercise 2.9.
Compute the weakest precondition of the following program with respect to the postcondition x < 10.
if x % 2 == 0 {
y := y + 3;
} else {
y := 4;
}
if y < 10 {
y := x + y;
} else {
x := 8;
}