Testing, Debugging, and Verification | TDA567/DIT082, LP2, HT2017 |
Exercises week 7 - Formal Verification, solution notes | |
Ideally you do the examples both on paper and in Dafny
1 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; } } } SolutionLet 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 ensures: (m = a || m = b || m = c) && (m <= a && m <= b && m <= c)Write an implementation and prove the correctness of it. SolutionImplementation: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 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. Solutionmethod 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 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. SolutionLoop invariant:invariant (sq1 == sq2 && sq1 * sq1 == n) || (sq1 < sq2 && sq1 * sq1 < n && sq2 * sq2 >= n); Proof details left out.
5 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. SolutionLoop 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 | Srinivas Pinisetty, Dec 18, 2017 |