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
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 Srinivas Pinisetty, Dec 18, 2017