|
This lab is about formal verification using Hoare logic with updates
for a simple while-language, as presented in the lectures and in
this
paper.
You are supposed use the KeY-Hoare tool to verify the programs
formally. For downloading and instructions for how to get started,
look
at http://www.key-project.org/download/hoare/.
For examples of how to use KeY-Hoare, consult the slides from the
lectures and the above mentioned paper. Note there is a problem with
file locks if you're using Windows. When you get a syntax error while
loading a file into KeY-Hoare, you may have to quit the application
before being able to write any changes to the opened file. A bit
annoying since this is what you want to do when you have get syntax
error, but it's easy to work around.
Whenever you are asked to construct a proof by hand (not using the
KeY-Hoare system) you should go like this: first give the initial
Hoare triple with updates representing the problem. Each main step of
the proof should correspond to applying one Hoare rule (backwards).
State which rule you apply and also the result, which may be one or
several new Hoare triples with updates, or a logical formula. If the
programs contains several assignments in a row, you can apply the
assignment rule for all of them before presenting the resulting Hoare
triple.
- If the rule application resulted in a new Hoare triple, 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 constraints (Hoare triple or
formula), then pick one of them and continue proving that constraint.
When the first constraint 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 with several similar Hoare
triples. 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 prove something using KeY-Hoare you
should:
- Write a .key file corresponding to the Hoare
triple.
- Load the file in KeY-Hoare and carry out the proof.
- Finally save the proof in a .key.proof file.
IMPORTANT NOTE: If your proof does not close, send the unclosed .proof file anyway! In this way we can give you more effective feedback.
|
1
The following piece of code exchanges the values of two
integers, i and j, without the use of a temporary
store.
i = i - j;
j = i + j;
i = j - i;
The specification of the program is:
requires: i = _i & j = _j
ensures: i = _j & j = _i
_i and _j are logical constants.
a
Use Hoare logic 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.
b
Use KeY-Hoare to prove the correctness. See the general guideline for
that above.
2
A program which will be called isorttriple has the following specification:
requires: a <= b & a = _a & b = _b & c = _c
ensures: a <= b & b <= c &
(a = _a & b = _b & c = _c |
a = _a & b = _c & c = _b |
a = _b & b = _a & c = _c |
a = _b & b = _c & c = _a |
a = _c & b = _a & c = _b |
a = _c & b = _b & c = _a)
_a,_b and _c are logical constants. All
locations and terms are integers.
a
Give an implementation of isorttriple.
b
Prove by hand that your implementation is correct.
c
Prove the same thing in KeY-Hoare.
3
The following piece of code multiplies two integers.
res = 0;
if (n < 0) {
n = -n;
m = -m;
} else {
}
while (n>0) {
res = res + m;
n = n - 1;
}
n and m are the two integer inputs to the
program. res is the integer result. Note that you have to
apply the loop rule twice (although there is onle one loop), once
after the then-branch has been executed, and once after the
else-branch has been executed.
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.
b
Prove by hand that the program is correct with respect to your
specification. There are two similar cases in the proof, one for each
loop invariant. You only have to include one of these cases in the
hand made proof. Only partial correctness has to be taken into
account.
c
Prove the same thing in KeY-Hoare (both cases).
4
The following program calculates the factorial of a number.
r = 1;
i = 2;
while (i <= n) {
r = r * i;
i = i + 1;
}
The variables are integers. You are supposed to prove that the
program is correct wrt to a recursive definition of the factorial
function:
fac(1) = 1 &
\forall int m; (m > 1 -> fac(m) = m * fac(m - 1))
This definition has to be included in the precondition and the loop
invariant when you use KeY-Hoare. fac has to be added as a
logical function in KeY-Hoare, see lecture slides for more details.
The full specification of the program is
requires: n = _n & n > 0 &
fac(1) = 1 &
\forall int m; (m > 1 -> fac(m) = m * fac(m - 1))
ensures: r = fac(_n)
_n is a logical integer constant and fac is a
function from integers to integers (declared as int
fac(int)).
a
Prove partial correctness of the program using KeY-Hoare.
b
Prove termination of the program using KeY-Hoare.
|
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 - Answers to questions 1a, 2a, 2b, 3a and 3b
- exchange.key and exchange.key.proof - Answer to question 1b
- isorttriple.key and isorttriple.key.proof - Answer to question 2c
- multiply.key and multiply.key.proof - Answer to question 3c
- factorial.key and factorial.key.proof - Answer to question 4a
- factorialt.key and factorialt.key.proof - Answer to question 4b
Remark: No need to be more complex than this; avoid package declarations, avoid to add unnecessary files such as hidden files or folders produced by your text editor, for instance.
Submission deadline is: (none)
Deadline for passing the lab is: (none)
|
|