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

Lab 3 - Formal Verification

This lab is about formal verification using the weakest pre-condition calculus, as presented in the lectures and in the book by Gries (see literature list) .

You may be asked to implement and check some programs in Dafny, as well as constructing proofs by hand.

Whenever you are asked to construct a proof by hand you should go like this: first state an expression for the weakest precondition of the program. Then, proceed to calculate the weakest precondition of the program by applying the appropriate inference rules. If required, show that it follows from the preconditions. Each main step of the proof should correspond to applying one of the Weakest Precondition calculus rules. State which rule you apply and also the result, which may be one or several new statements or logical formula.

  • If the rule application resulted in a new statement, simply continue with the proof in the same way.
  • If it resulted in a logical formula, explain why the formula is valid.
  • If it resulted in several new subgoals or conjuncts, you may pick one of them and continue proving that one. When the first subgoal has been proved true, don't forget that you have to go back and prove the other ones, too. Number the intermediate results if there is any danger of confusion.
  • If you used the loop invariant rule, clearly state which formula you are using as invariant.

The proofs can be rather lengthy. You can copy and paste to avoid excessive typing. When you are dealing with large formulas in the pre or postcondition you can introduce names to abbreviate them. Just keep in mind that when you are applying an update to a formula you have to unfold the abbreviation first before you apply the update.

Whenever you are asked to implement something using Dafny you should:

  1. Write a .dfy file corresponding to the program.
  2. Make sure Dafny can prove your program correct according to specification.

1

Below is the familiar Dafny program for computing an absolute value of a number

method Abs(x : int) returns (y : int) 
  ensures 0 <= y;
  ensures 0 <= x ==> y == x;
  ensures x < 0 ==> y == -x;
{
  if (x < 0)
   {y := -x;}
  else
   {y := x;}
}

Use the weakest precondition calculus to prove that the program is correct with respect to the specification. Construct a proof by hand. See the general guidelines for doing that above.


2

Below is a small Dafny program

method Q2(x : int, y : int) returns (big : int, small : int) 
  ensures big > small;
{
  if (x > y)
   {big, small := x, y;}
  else
   {big, small := y, x;}
}

a
Dafny will not be able to prove the above program correct (try it!), as its specification is incomplete. Your task is to figure out exactly why the proof fails, and from there derive the missing part of the specification (the postcondition or method body should not be changed). Do this by applying the rules for the weakest precondition calculus for the above program (by hand). Show each step of the derivation.

b
Show that your answer from part (a) allow the proof of correctness to go through. Also add the missing part of the specification to the above method, and verify the program in Dafny to make sure it is correct.


3

The following method multiplies two integers.

method Q3(n0 : int, m0 : int) returns (res : int)
  
{
  var n, m : int;
  res := 0;
  if (n0 >= 0) 
       {n,m := n0, m0;} 
  else 
       {n,m := -n0, -m0;}
  while (0 < n) 
  { 
    res := res + m; 
    n := n - 1; 
  }
}

n0 and m0 are the two integer inputs to the program. res is the integer result, recall that Dafny do not allow you to assign to the parameters to a method, only to local variable, why we declare the variables n and m.

a
What should the specification of the program be? You can of course always give a silly specification for which the program is correct, but this will not be considered a correct specification.

Complete the program with specifications and invariants in Dafny and check that it verifies. If you find it difficult to come up with the correct invariant, try starting on part (b) below to see if it offers any insights...

b
Prove by hand that the program is correct with respect to your specification. Follow the steps in the "checklist" for proving loops correct from the lecture notes. See also Chapter 11 of [Gries].


4

The factorial function, written often written n! computes the product of all numbers from 1 up to n, e.g. !3 = 1 * 2 * 3 = 6. The following Dafny program calculates the factorial of a number.

method ComputeFact(n : nat) returns (res : nat)
  requires n > 0;
  ensures res == fact(n);
 {
  res := 1;
  var i := 2;
  while (i <= n) 
  {
    res := res * i;
    i := i + 1;
  }
 }
The variables are natural numbers. You are supposed to prove that the program is correct wrt to a recursive definition of the factorial function, defined mathematically as:
  fact(1) = 1
  fact(m) = m * fact(m - 1)

a
Complete the specification so that Dafny is able to prove ComputeFact correct.

b
Prove correctness of the loop using the checklist for proving loops correct from the lecture notes. See also Chapter 11 of [Gries].


Reporting

Upload an archive LAB3.zip (or rar, tar.gz, tar as you wish) containing the following files, using the Fire report system:

  • lab3.txt - Your proofs: answers to questions 1, 2a, 2b, 3b and 4b
  • Q2.dfy Answer to question 2b
  • Q3.dfy Answer to question 3a
  • Fact.dfy Answer to question 4a

Remark: No need to be more complex than this; avoid to add unnecessary files such as hidden files or folders produced by your text editor, for instance.


Submission deadline is: Tuesday, December 20 2016 23:59
Deadline for passing the lab is: Friday, January 6 2017



Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools Atze van der Ploeg, Sep 28, 2015