Lab 2 - Specification and Verification of Programs using KeY
Ensure that you are using the specific KeY 2.7 release linked from the tools page when solving these problems, as the save format is not stable between KeY versions. If it is not possible to open your saved files with this version of KeY, your Fire submission will be rejected without review and you will have to resubmit with compatible save files.
Problem 1: First-Order Logic
Prove the validity of the following untyped first-order formula using the
$$(\forall x; ((r(x) \implies \lnot g(x)) \land (g(x) \implies \lnot
r(x)))) \land (\forall x; \forall y; (i(x,y) \implies r(x) \lor r(y)))
(\lnot \exists x; \exists y; (i(x,y) \land g(x) \land g(y)))
\land (\exists x; \exists y; i(x,y) \implies \exists z; r(z))$$
One could, for example, imagine that the formula speaks about traffic lights placed at
intersections, where the unary predicates r and g speak about a
traffic light being red or green respectively, and the binary
predicate i can be interpreted as two lights standing at the same
Your task is to first formulate the problem in a KeY problem file,
and then load the file in KeY and prove it using the first-order logic rules presented
during the lectures, as summarized in this PDF.
You are not allowed to use any other rules.
In particular letting KeY auto-prove the formula will not help you much,
as the proof is vastly different and uses many rules which are forbidden.
For the lab report, you should save your KeY proof into a file. In KeY, once you are done with the proof, go to File and then choose Save (use as extension .proof).
Hint: If you are generating the rules instAll and instEx through
drag-and-drop, you can instead generate the allowed rules allLeft and exRight by
simply dragging the formula onto the term rather than the other way around.
Problem 2: JML Specifications
NumericTextBox.java contains the
NumericTextBox. Its methods and fields are commented,
informally describing the specifications for the class. Your assignment is to
formalize these specifications using JML. Please read the entire Java file,
especially the comments, before starting.
We will return to this Java file in problem 4 (below), but for now you do not need to implement or prove anything.
Problem 3: Verification with KeY
BinarySearch that can be found in the file
BinarySearch.java contains an array of numbers which it searches for a query using the binary search algorithm.
Some implementations and JML-specifications are given already. In this task you will practise verification with KeY.
Sometimes KeY cannot find proofs in a fully automatic fashion.
In this part of the lab you will need to interact with KeY in order to provide the correct information so that the prover can find the proofs.
Some proofs can be lengthy and it is easy to get lost in the mare magnum of proof steps.
However, constructing proofs is a creative process, in the same way writing software is a creative process (and to some extent, the mechanical aspects of pen-and-paper proofs are supposed to be handled by the KeY system already).
Consequently, everyone approaches proofs differently, so it is difficult to give general guidelines on how to close KeY proofs, but we hope the following guidelines might be of some use:
Read carefully the contracts you need to prove.
It is important that you understand what is the property you need to prove before you hit the play button.
If you get stuck, revisit the property and make sure you really understand what you are trying to prove.
Analyse the proof tree.
Specially check the branching points of the proof.
They usually provide useful hints on why a proof cannot be close.
Here it is also very important that you understand what KeY is trying to prove in a particular branch.
Looking at the splitting node (small light-blue folders in the proof tree) gives you information about the goal to prove.
When you click on the folder, look at proof obligation and try to understand what needs to be proven in the branch.
Consult the KeY book.
We recommend you to have a look at section 15.3 of the KeY book as complementary material to do this lab.
This section includes various hints on how to effectively use KeY for verification of large programs.
Task 3.1: Normal Behaviour
Verify with KeY that the method
performBinarySearch meets its specification.
Make sure that "Method Treatment" under "Proof Search Strategy" is set to "None" before you start.
Note that the method
performBinarySearch consists in four method calls.
When KeY encounters a method call you can choose to perform two different actions:
In order to determine which one to apply you need to look a the contract of the method in question.
If the contract contains useful information to close the proof you should use the contract.
Otherwise, it is better to inline the method.
- Inline method: example
- Use method contract: example
Hint: It might be necessary to use the rules AllLeft and/or ExLeft to manually instantiate some of the quantified variables of the contracts.
Task 3.2: Exceptional Behaviour
You may have noticed that the method
eliminateDuplicates does not meet
its specification for the exceptional behaviour case. Change the
implementation of the
eliminateDuplicates method so that it meets its
specification for exceptional behaviour and verify that this is indeed
the case. You may modify the setting for method treatment to any option of your choice for this task.
Hint: You might have to switch the method treat "Method Treatment" under "Proof Search Strategy" from "None" to "Contract".
Task 3.3: Invariants
Drawing that you can find in the file
Drawing.java contains a two-dimensional array that models a canvas onto which lines can be drawn. When a point is coloured, the corresponding entry in the array is set to true. The class has two invariants. One specifies that the canvas must be square and one specifies that every coloured point on the canvas must be part of either a horizontal or a vertical line.
The proof of every method contract also automatically includes the invariants as assumptions and as proof goals. Thus, showing any method contract also includes proving that the respective method preserves the invariants. We will now take a closer look at proving invariants by proving contracts without postconditions so that the proof obligations are reduced to the preservation of invariants.
In this task you will verify two such contracts. Before you start make sure both "Method Treatment" and "Loop Treatment" under "Proof Search Strategy" are set to "None", and "One Step Simplification" is set to "Enabled". When symbolic execution reaches a call to another method, or a loop, you will have to perform interactive steps in order to continue with the proof.
Prove that the method
drawMultiple() preserves the invariants. In order to do so, under "Proof Search Strategy" set the option "Class axiom rule" to "Delayed".
First set the "Proof Search Strategy" option "Class axiom rule" (back) to "Free". The task is to prove that the method
drawVertical(int depth) preserves the class invariants. For this, you will have to find and correct a small mistake in the loop invariant.
One way of doing this is to attempt the proof using the erroneous invariant, as given, and inspect the goal(s) that cannot be closed. For that, set the "Max. Rule Applications" down to 1000. The branch "Initially Valid" can be closed using "apply rules automatically here" (which is offered when the mouse is on the sequent arrow). To discover the error in the loop invariant, apply rules automatically on the branch "Body Preserves Invariant", prune the tree before the CUT nodes that branch over the
length of canvas. Watch out for formulas on both sides of the sequent which are similar but not equal. Once you have corrected the mistake, restart the proof, with "Max. Rule Applications" set to 20k, such that the proof will only require interaction upon reaching the loop and the remaining proof works automatically.
Problem 4: Further Verification with KeY
After the warm-up with KeY in problem 3, we will now return to the Java file
NumericTextBox.java from problem 2. Your task is now to provide implementations for the methods in the class
NumericTextBox such that your implementations satisfy the JML specifications you wrote in problem 2, and then prove that your implementations indeed satisfy your specifications.
Hint: Remember that you must provide a loop invariant when using KeY to reason about non-trivial loops. Furthermore, to be able to show that a loop always terminates you must provide a
decreasing clause. Lastly, do not forgot that loop invariants have their own
assignable clauses, separate from any method specifications.
- The files required in the submission of this lab are:
- A text report named Report_Lab2.txt describing your solutions to problem 3 and 4 (what you did and why)
- All modified Java files
- All KeY proofs (as instructed above, please make sure you are using the correct KeY version)
- Do not submit your files as an archive file (such as zip, tar.bz2, tar.gz or similar)
- Make sure to submit the report in plain text format (.txt). Avoid other formats as this may cause delays in grading your submission.
- Submit via Fire