Question 1: Pure methods should not be methods!
Let's start with a warm up question: Below is the familiar Dafny
program for computing an absolute value of a number. However, instead
of a function, the author made a design mistake and decided to write
it as a method!
method Abs(x : int) returns (y : int)
// return value doesn't deviate from intended value
ensures 0 <= x ==> y == x;
ensures x < 0 ==> y == -x;
// return value is greater or equal to zero
ensures 0 <= y;
{
if (x < 0)
{ y := -x; }
else
{ y := x; }
}
Your task is to use the weakest precondition calculus (wp(S, R) ) to
prove that the program is correct with respect to its specifications.
Construct a proof by hand.
- Write down the initial weakest precondition of the program (based on its postconditions only)
- Construct the correctness proof by hand using
wp(S, R)
- [Open question] Why is this method considered as a design mistake?
If you have doubt about how to write the correctness proof, see the general guidelines.
Question 2: Missing specs or wrong program?
Below is a small Dafny program:
Dafny will NOT be able to prove the above program correct (try it!), as its specification is incomplete.
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;}
}
Your task is to figure out exactly why the proof fails, and from there derive a verfiable version of this program.
- Describe in words why is the program not verifiable?
- With only description it can be difficult to convince others that the mistake is really there! Your second task is to use
wp(S, R) to show the postcondition really fails to hold according to weakest precondition calculus
There are many ways of fixing this program:
- Without changing the postcondition nor the method body, try to fix this program so that it becomes verifiable
- Without adding new precondition nor changing the method body, try to fix this program so that it becomes verifiable
- [Bonus: think outside the box] Without changing its specification, can this program be verifiable?
(If you managed to answer the bonus question above, can you try to go back to original question and refine the specifications so the method is more precisely described by its specs?)
Question 3: Correct program AND missing specs!
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;
}
}
- Why can't we use the inputs directly? (n0, m0)
- What IS the purpose of method? In other words, what should the
specification (postcondition(s)) 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.)
- 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].
[Hint] If you successfully figure out the method's purpose, try to
include additional specification so that you can demonstrate the
correctness of this program against standard library function.
Question 4: Factorial!
The factorial (written often written as n! in mathematics) computes the
product of all numbers from 1 up to n, given positive n. (for example: 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 with respect to a recursive definition of the factorial
function, defined mathematically as:
fact(1) = 1
fact(m) = m * fact(m - 1)
- Complete the specification so that Dafny is able to prove
ComputeFact correct.
- 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:
LAB3.zip ( or tar )
|
|- Q1.dfy
|- Q2.dfy
|- Q3.dfy
|- Q4.dfy
|
|- Appendix/
| |- More_material_if_needed
Remark: Please avoid adding unnecessary files, this would speed up the grading process which would make the comments available earlier.
Submission deadline is: Wednesday, December 20 2017 23:59
Deadline for passing the lab is: Wednesday, January 10 2017
|
|