Hello, if you have any need, please feel free to consult us, this is my wechat: wx91due
CSSE3100/7100 Reasoning about Programs
Week 4 Exercises
Exercise 4.1.
For each of the following uses of loop specifications, indicate whether or not the loop's initial proof obligation is met and whether or not the postcondition following the loop can be proved to hold.
a) x := 0;
while x != 100
invariant true
{ x == 100 }
b) x := 20;
while 10 < x
invariant x%2 == 0
{ x == 10 }
c) x := 20;
while x < 20
invariant x%2 == 0
{ x == 20 }
d) x := 3;
while x < 2
invariant x%2 == 0
{ x%2 == 0 }
e) x := 0;
while x < 100
invariant 0 <= x < 100
{ x == 25 }
Exercise 4.2.
For each program, determine why the postcondition is not provable and strengthen the invariant so that it holds on entry to the loop and suffices to prove the postcondition.
a) i := 0;
while i < 100
invariant 0 <= i
{ i == 100 }
b) i := 100;
while i > 0
invariant true
{ i == 0 }
c) i := 0;
while i < 97
invariant 0 <= i <= 99
{ i == 99 }
d) i := 22;
while i%5 != 0
invariant 10 <= i <= 100
{ i == 55 }
Exercise 4.3.
Consider the following program fragment:
x := 0;
while x < 100
{
x := x + 3;
}
{ x == 102 }
Write a loop invariant that holds initially, is maintained by the loop body, and allows you to prove the postcondition after the loop.
Exercise 4.4.
For each of the following methods, write a loop invariant and a decreases clause that would allow you to prove the method is totally correct. The proof is not required.
method UpWhileLess(N: int) returns (i: int)
requires N >= 0
ensures i == N
{
i := 0;
while i < N {
i := i + 1;
}
}
method UpWhileNotEqual(N: int) returns (i: int)
requires N >= 0
ensures i == N
{
i := 0;
while i != N {
i := i + 1;
}
}
method DownWhileNotEqual(N: int) returns (i: int)
requires N >= 0
ensures i == 0
{
i := N;
while i != 0 {
i := i - 1;
}
}
method DownWhileGreater(N: int) returns (i: int)
requires N >= 0
ensures i == 0
{
i := N;
while i > 0 {
i := i - 1;
}
}
Let Power be defined as
ghost function Power(n: nat): nat {
if n == 0 then 1 else 2*Power(n - 1)
}
and ComputePower be the method
method ComputePower(N: int) returns (y: nat)
requires N >= 0
ensures y == Power(N)
{
y := 1;
var x := 0;
while x != N
invariant 0 <= x <= N
invariant y == Power(x)
{
x, y := x + 1, y + y;
}
}
a) Use weakest precondition reasoning to show that ComputePower is partially correct.
b) Use weakest precondition reasoning to show that ComputePower is also totally correct. You will need to choose a suitable termination metric.