Software Engineering using
Formal Methods		 TDA293/DIT270, LP1, HT2015

Lab 2 - Specification and Verification of Programs using KeY

This lab consists of the following three problems:

Problem 1: First-Order Logic

Prove the validity of the following untyped first-order formula using the sequent calculus. $$(\forall x; ((r(x) \rightarrow \neg g(x)) \wedge (g(x) \rightarrow \neg r(x)))) \wedge (\forall x; \forall y; (i(x,y) \rightarrow r(x) \vee r(y))) \rightarrow (\neg \exists x; \exists y; (i(x,y) \wedge g(x) \wedge g(y))) \wedge (\exists x; \exists y; i(x,y) \rightarrow \exists z; r(z))$$ You may assume 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.

To solve this problem you must first formulate it in a KeY problem file. As KeY does not have the notion of untyped, you must define a new sort which all predicates and variables will reference. Also define the predicates required in order to formulate the problem. Now load the file in KeY and prove it using the first-order logic rules presented during the lectures, Sequent Calculus Rules. 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.

Reporting

For 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 Specifications

The file NumericTextBox.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 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.

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. You may have to inline methods or make use of certain method contracts to prove your goal. Furthermore, it might be necessary to use the rules AllLeft and/or ExLeft. Hint: Note that the specification of report() is not very meaningful in the context of the proof you have to solve in this exercise. Therefore, you might not need to use the contract of the report method.

Inlining methods or using contracts

Here you have an example on how to inline a method: example
Here you have an example on how to use the contract of a method: example


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: It might be possible that you have to switch the method treat "Method Treatment" under "Proof Search Strategy" from "None" to "Contract".

Task 3.3: Invariants

The class 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, 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.
  • a) 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".
    Hint: To symbolically execute calls to other methods, KeY has to either use the contracts of that other method or inline its implementation.
  • b) 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 possibility is that you find the mistake just by inspecting Drawing.java, and prove the corrected version. For that, set the "Max. Rule Applications" in the "Proof Search Strategy" to 20k. The other possibility is that you 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 1k. 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.

Submission Guidelines

  • The files required in the submission of this lab are:
    • A text report named Report_Lab2.txt describing your solution to problems 1-3.
    • All modified Java files.
    • All KeY proofs.
  • Submit via Fire


Home | Course | Schedule | Exam | Exercises | Labs | Eval | Tools W. Ahrendt , Oct 21, 2015