Solutions Download

Propositional Logic and KeY

Sequent Calculus

Using KeY

• The book chapter "Using the KeY Prover" of the KeY book gives a good introduction on how to use the KeY prover.
• See the tools page for a download link to KeY.

Proving with KeY

Here are the KeY files for the previous exercise. Your task is now:

1. Replay your solution from the previous exercise in KeY by hand. Use only those rules you have applied in the pen-and-paper version and in exactly the same order.
2. Instead of replaying the proof by hand, let KeY find the solution automatically (check that the number of max rule applications is at 5000). The prover used rules which were not presented in the lecture, among them a rule called replace_known_left. Describe what the rule does and give a natural language justification, why this rule is sound.

First-Order Logic

Exercise 1

1. Prove the following formulas with pen and paper:
   1. $$\forall x; p(x) \lor \forall x; c(x) \implies \forall x; (p(x) \lor c(x))$$
   2. $$\lnot (\exists x; p(x)) \implies \forall x; (\lnot p(x))$$
   3. $$(\forall x; p(x) \implies \exists x; q(x)) \implies \exists x; (p(x) \implies q(x))$$
   4. $$\forall x; f(g(x)) = g(x) \land g(a) = b \implies f(b) = g(a)$$
   5. $$\forall x; (p(x) \lor q(x)) \implies \lnot (\exists x; (\lnot p(x) \land \lnot q(x)))$$
   6. $$[(\forall x; R(x,x) \land \forall x, y, z; (R(x,z) \land R(y,z))) \implies R(x,y))] \implies [\forall x, y; R(x,y) \implies R(y,x)]$$
   7. $$[(\forall x; R(x,x)) \land (\forall x, y, z; (R(x,z) \land R(y,z)) \implies R(x,y))] \implies [\forall x, y, z; (R(x,y) \land R(y,z)) \implies R(x,z))]$$
2. Prove now the above formulas assisted by KeY. Don't apply rules automatically! You find the necessary input files here.

JML

Exercise 2

Write JML expressions which precisely describe the following:

2a
All elements in b[j..k] are zero.

2b
All zeros of b[0..n-1] are in b[j..k].

2c
It is not the case that all zeros of b[0..n-1] are in b[j..k].
(Write this in two ways, once using negation ('!') an once avoiding negation.)

2d
b[0..n-1] contains two zeros.

2e
b[0..n-1] contains at least two zeros.

2f
b[0..n-1] contains at most two zeros.
(First write a solution, then reflect on this: One example of an array that contains at most two zeros is an array which has only one element, i.e., it has length one. Does your solution evaluate to true if b has only one element?)

2g
Specify a method public static void reverse( int[] b ) which reverses the order of elements in b.

Exercise 3

Consider the class EntryList:

/* A simple linked list of entries.
 */
public class EntryList {
  Object first;
  EntryList rest;

  EntryList( Object first, EntryList rest ) {
    this.first = first;
    this.rest = rest;
  }

  // some methods, among them:
  int size() {
    // ...
  }
}

Specify size() using JML. This is not as trivial as one might think. Please think about it before the exercise session. Even if you try in vain, having tried will make you remember the key idea behind the solution.

Exercise 4

In this assignment, we are going to specify an implementation of a Queue. We do not actually implement it.

Consider the following half-done class description of a Queue:

public class Queue {
  Object[] arr;
  int size;
  int first;
  int next;

  Queue( int max ) {
    // ...
  }

  public int size() {
    // ...
  }

  public void enqueue( Object x ) {
    // ...
  }

  public Object dequeue() {
    // ...
  }
}

Give a JML specification of the Queue. It should consist of: class invariant(s), and pre- and post-conditions for each method.

Exercise 5

Your task is to provide specifications for a class implementing a maze game. A maze is described as a two dimensional array, where all rows have the same number of columns.

The class Maze declares

• constants MOVE_X encoding different move directions (up, down, left, right).
• constants EXIT, FREE and WALL encoding the kind of a maze cell, i.e., if it is occupied by a wall, the exit or free.
• two integer fields playerRow and playerCol with the current position of the player.
• a two-dimensional array field of integer type maze representing the maze itself.

The skeleton for the Maze class:

public class Maze {
  // CONSTANTS -- MOVE
  public final static int MOVE_UP    = 0;
  public final static int MOVE_DOWN  = 1;
  public final static int MOVE_LEFT  = 2;
  public final static int MOVE_RIGHT = 3;

  // CONSTANTS -- FIELDS
  public final static int FREE = 0;
  public final static int WALL = 1;
  public final static int EXIT = 2;

  /**
   * The playfield is given as a rectangle where
   *
   *   - Walls are represented by entries of value Maze.WALL ('1')
   *   - The exit is represented as an entry of value Maze.EXIT ('2')
   *   - All other entries are MAZE.FREE ('0')
   *   - A playfield has exactly one exit.
   *   - The first number determines the column, the second determines
   *     the row. Row and column numbers start at 0.
   *   - Each row has the same number of columns.
   */
  private int[][] maze;

  /**
   * Player position:
   *
   *   - The position of a player must always denote a field inside the
   *     maze which is not a wall
   */
  private int playerRow, playerCol;

  public Maze(int[][] maze, int startRow, int startCol) {
    this.maze = maze;
    // set player on start position
    this.playerRow = startRow;
    this.playerCol = startCol;
  }

  /**
   * Returns true if the player has reached the exit field;
   * the method does not affect the state.
   */
  public boolean won() {
    // TO BE IMPLEMENTED
    throw new RuntimeException();
  }

  /**
   * A move to position (newRow,newCol) is possible iff the
   * field is inside the maze and free (i.e. not a wall);
   * the method does not affect the state.
   */
  public boolean isPossible(int newRow, int newCol) {
    // TO BE IMPLEMENTED
    throw new RuntimeException();
  }

  /**
   * Takes a direction and performs the move if possible, otherwise
   * the player stays at the current position; the direction must be
   * one of the defined move directions (see constants
   * MOVE_xyz). The return value indicates if the move was successful.
   */
  public boolean move(int direction) {
    // TO BE IMPLEMENTED
    throw new RuntimeException();
  }
}

Your task is now to provide

1. JML invariants specifying that:
   1. the maze is non-null (i.e., the field itself is not null and so are its elements).
   2. each row of the maze has the same number of columns (i.e., the maze has rectangular shape).
   3. the player position is inside the maze and not occupied by a wall.
   4. each cell inside the maze is either free, a wall or an exit.
   5. there is at most one exit.
2. normal_behavior method specifications for each method which reflect the natural language comment as complete as possible.