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:
- Write a .dfy file corresponding to the program.
- 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
|
|