Testing, Debugging, and Verification TDA567/DIT082, LP2, HT2015

Exercises week 6 - Formal Verification, solution notes

Ideally you do the examples both on paper and in Dafny

1
Prove the correctness of the following silly program.

```method M (x0 : int) returns (x : int)
ensures (x0 < 3 ==> x == 1) && (x0 >= 3 ==> x < x0);
{
x := x0 - 3;
if (x < 0) {
x := 1;
} else {
if (true) {
x := x + 1;
} else {
x := 10;
}
}
}
```

### Solution

Let R stand for (x0 < 3 ==> x == 1) && (x0 >= 3 ==> x < x0)
```
By Seq. rule:
wp(x:= x0-3, wp(if (x < 0) .., R)))

By Conditional rule:
wp(x:= x0-3,
( (x < 0) ==> wp(x:= 1, R)
&&
(x >= 0) ==> wp(if (true)..., R))

By Assignment rule to first conjunct:
wp(x:= x0-3,
( (x < 0) ==> R[x -> 1] (trivially true)
&&
(x >= 0) ==> wp(if (true)..., R)))

By Conditional rule
wp(x:= x0-3,
True &&
(x >= 0) ==> (true ==> wp(x:= x+1, R)
&&
false ==> wp(x:=10, R) (trivially true)

By Assignment rule
wp(x:= x0-3,
(x >= 0) ==> R[x -> x+1])
&&
true
Simplify
wp(x:= x0-3,
(x >= 0) ==> (x0 < 3 ==> x+1 == 1) && (x0 >= 3 ==> x+1 < x0))

By Assignment rule
(x0-3) >= 0 ==> (x0 < 3 ==> x0-3+1 == 1) && (x0 >= 3 ==> x0-3+1 < x0)

Simplify
x0 >= 3 ==> (x0 < 3 ==> x0 == 3) && (x0 >= 3 ==> x0-2 < x0)

Simplify
x0 >= 3 ==> (false ==> x0==3) && (true ==> x0-2 < x0)

Simplify
x0 >= 3 ==> true.

```

2
Given the specification:

``` ensures: (m = a || m = b || m = c) && (m <= a && m <= b && m <= c)
```
Write an implementation and prove the correctness of it.

### Solution

Implementation:
```method M2(a : int, b : int, c : int) returns (m : int)
ensures (m == a || m == b || m == c);
ensures (m <= a && m <= b && m <= c) ;
{
m := a;
if (b < m)
{ m := b; }
if (c < m)
{ m := c; }
}
```
Proof:
Let R = (m == a || m == b || m == c) && (m <= a && m <= b && m <= c)
```By Seq. rule (twice)
wp(m:=a, wp(if (b < m)..., wp(if (c < m)..., R))))

By Conditional rule
wp(m:=a,
wp(if (b < m)...,
(c < m ==> wp(m:= c, R)
&&
!(c < m) ==> R)

By Assignment rule
wp(m:=a,
wp(if (b < m)...,
(c < m ==> (c==a || c==b ||c==c) && (c <= a && c <= b && c <= c)
&&
!(c < m) ==> R))

By Conditional rule, and simplification:
wp(m:=a,
(b < m ==> wp(m:=b, (c < m ==> c <= a && c <=b) &&
(m <= c ==> R)))
&&
!(b < m) ==> (c < m ==> c <= a && c <=b) &&
(m <= c ==> R)

By Assignment rule
wp(m:=a,
(b < m ==> (c < b ==> c <= a && c <= b) &&
(b >= c ==> (b == a || b == b || b == c) && (b <= a && b <= b && b <= c))
&&
!(b < m) ==> (c < m ==> c <= a && c <=b) &&
(m <= c ==> R)

Simplify
wp(m:=a,
(b < m ==> (c < b ==> c <= a && c <= b) &&
(b <= c ==> (b <= a && b <= c))
&&
!(b < m) ==> (c < m ==> c <= a && c <=b) &&
(m <= c ==> R)

Apply Assignment
(b < a ==> (c < b ==> c <= a && c <= b) &&
(b <= c ==> (b <= a && b <= c))
&&
!(b < a) ==> (c < a ==> c <= a && c <=b) &&
(a <= c ==> R[m -> a])

First conjunct simplifies to true, simplify second conjunct to get
true
&&
!(b < a) ==> true &&
(a <= c ==> (a == a || a == b || a == c)
&& (a <= a && a<= b && a <= c)

Simplify
true

```

3
Prove the partial correctness of:

```method M3(x : int, y : int) returns (q : int, r : int)
requires x >= 0 && y > 0;
ensures q * y + r == x && r >= 0 && r < y;
q := 0;
r := x;
while (r >= y) {
r = r - y;
q = q + 1;
}
```
The program divides x by y. q contains the quotient afterwards and r the remainder.

### Solution

```method M3(x : int, y : int) returns (q : int, r : int)
requires x >= 0 && y > 0;
ensures q * y + r == x && r >= 0 && r < y;
{
q := 0;
r := x;
while (r >= y)
invariant q * y + r == x && r >= 0 && y > 0;
decreases r;
{
r := r - y;
q := q + 1;
}
}

```

Proof:
Let Q = x >= 0 && y > 0
Let R = q * y + r == x && r >= 0 && r < y && y > 0

Folowing the 5 step cheklist for proving loops correct from the lecture notes.

(1) Show that the invariant holds prior to entering the loop. This amount to showing

```Q ==> wp(q:=0; r:=x, I)

By Seq rule followed by Assignment rule we get
x >= 0 && y > 0 ==> 0 * y + x == x && x >= 0 && y > 0

Simplify
x >= 0 && y > 0 ==> 0+x==x && x >= 0 && y > 0

True
```
(2) Show that the invariant is preserved by the loop. This amount to showing
```I && B ==> wp(r := r - y; q := q + 1, I)

By Seq rule followed by Assignment rule
I && (r >=y) ==> q+1 * y + r-y == x && r-y >= 0 && y > 0

Simplify
q * y + r == x && r >= 0 && r >= 0 && y > 0 && r >=y ==>
q+1 * y + r-y == x && r-y >= 0 && y > 0

Simplify
q * y + r == x && r >= 0 && r >= 0 && y > 0 && r >=y ==>
(q*y + y) + r-y == x && r-y >= 0 && y > 0

First conjunct, (q*y + y) + r-y == x is identical to the first premise. The second conjunct, r-y >= 0, follows
from premises r >=0 && r >=y, and y > 0 follows trivially from the
corresponding premise.
```
(3) Show that the postcondition hold after the loop exits. This amount to showing
```
I && !(r >=y) ==> R

q * y + r == x && r >= 0 && y > 0 && r < y ==>
q * y + r == x && r >= 0 && y > 0 && r < y

Which follows directly from the invariant and negated loop guard.
```
(4) Show that the variant is bounded from below by 0, as long as the loop has not terminated.
```
I && (r >=y) ==> r > 0

x >= 0 && y > 0 && q * y + r == x && r >= 0 && y > 0 && r >= y ==> r > 0

Which follows directly from the conjunct y > 0 and loop guard r >= y.
```
(5) Show that the variant decrease on each loop iteration. This amounts to proving that:
```
I && (r >=y) ==> wp(V1:= V; r := r - y; q := q + 1, V < V1)

By Sequential and Assignment rules, we obtain

I && (r >=y) ==> wp(V1 := r, r-y < V1)

By Assignment rule
I && (r >=y) ==> (r-y < r)

This follows from the loop guard: r >= y and conjunct y > 0.
```
This concludes the proof.

4
Find the missing invariant which allows Dafny to prove correctness of the following program. If you have time, also prove the partial correctness on paper:

```method M4 (n : int) returns (sq1 : int, sq2 : int)
requires n >= 0 && n * n >= n;
ensures  (sq1 == sq2 && sq1 * sq1 == n) ||
(sq1 + 1 == sq2 && sq1 * sq1 < n && sq2 * sq2 >= n);
{
sq1 := 0;
sq2 := n;
var mid := 0;
while (sq2 - sq1 > 1)
{
mid := (sq1 + sq2) / 2;
if (mid * mid == n) {
sq1 := mid;
sq2 := mid;
} else {
if (mid * mid < n) {
sq1 := mid;
} else {
sq2 := mid;
}
}
}

}
```
The program uses monotonicity to calculate the integer approximation of the square root of n.

### Solution

Loop invariant:
```invariant (sq1 == sq2 && sq1 * sq1 == n) || (sq1 < sq2 && sq1 * sq1 < n && sq2 * sq2 >= n);
```

Proof details left out.

5
Provide Dafny with the missing annotations required to prove the total correctness of the program below. If you want, also prove it correct on paper.

```method M5(a0 : int, b0 : int) returns (c : int)
requires a0 >= 0 && b0 >= 0;
ensures c == a0+b0;
{
c := 0;
var a, b, g, m := a0, b0, 1, 0;
while (a > 0 || b > 0)

{
m := m + a % 2 + b % 2;
a := a / 2;
b := b / 2;
c := c + g * (m % 2);
g := 2 * g;
m := m / 2;
}
c := c + g * m;
}

```
The program performs bitwise addition of a and b. m is the carry bit.

### Solution

Loop invariant:
```invariant a0 + b0 == c + g * (a + b + m) && a >= 0 && b >= 0;
```
This time Dafny cannot guess the variant automatically. We need to supply the variant: decreases a+b;
Proof details left out.

Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools | Links Atze van der Ploeg, Dec 10, 2015