Formal Methods for Software Development | TDA294/DIT271, LP1, HT2017 |
Lab 2 - Specification and Verification of Programs using KeYThis lab consists of three problems. Please ensure that you are using the latest version of KeY when solving these problems (see the tools page), as the save format is not always stable between versions. If it is not possible to open your saved files with the latest version of KeY, your Fire submission will be rejected and you will have to resubmit it with compatible save files. Problem 1: First-Order LogicProve the validity of the following untyped first-order formula using the sequent calculus. $$(\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))) \implies (\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 intersection.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. 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. ReportingFor Part 1 of the assignment you can 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). Problem 2: JML SpecificationsThe fileNumericTextBox.java contains the
unimplemented class 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. You do not need to implement or prove
anything.
Problem 3: Verification with KeY
The class 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:
Task 3.1: Normal Behaviour
Verify with KeY that the method 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 BehaviourYou may have noticed that the method Hint: You might have to switch the method treat "Method Treatment" under "Proof Search Strategy" from "None" to "Contract". Task 3.3: InvariantsThe classDrawing 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, toggle in the toolbar the (green) "aggregation of simplification rules", and make sure that both "Method Treatment" and "Loop Treatment" under "Proof Search Strategy" are set to "None". 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.
Submission Guidelines
| |
Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools | W. Ahrendt, Oct 10, 2017 |