Testing, Debugging, and Verification | TDA567/DIT082, LP2, HT2017 |
Exercises week 6 - 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; } } }
2 ensures: (m = a || m = b || m = c) && (m <= a && m <= b && m <= c)Write an implementation and prove the correctness of it.
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.
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.
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. | |
Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools | Links | Atze van der Ploeg, Nov 3, 2016 |