Solutions Download

Part II. Propositional Logic and KeY

Sequent Calculus

1. (p ∧ (p → q)) → q -------------- Modus ponens
2. ((p ∨ q) ∧ (p → q)) → q --------
3. ((p ∧ q) → r) → (p → (q → r)) -- Exportation
4. (p → q) → ¬ p ∨ q -------------- Material implication
5. ¬(p ∧ q) → ¬ p ∨ ¬ q ----------- De Morgan

Using KeY

The preprint of a book chapter of the new KeY book, called "Using the KeY Prover" (it has been spread via the Google group, and is also available via personal request from the course teacher), gives a good introduction on how to use the KeY prover.

For this exercise we are using the webstart version of KeY. (See the tools page.) Click "Open", which should start the Java Web Launcher. Choose "Run" when requested.

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 rules is sound.

First-Order Logic

Recommended

1(1-5, 7), 2, 5.

Exercise 1

1. Prove the following formulas with pen and paper:
   1. ∀ x; p(x) | ∀ x; c(x) -> ∀ x; (p(x) | c(x))
   2. !(∃ x; p(x)) -> ∀ x; (! p(x))
   3. (∀ x; p(x) -> ∃ x; q(x)) -> ∃ x; (p(x) -> q(x))
   4. ∀ x; f(g(x))=g(x) & g(a)=b -> f(b)=g(a)
   5. ∀ x; (p(x) | q(x)) -> ! (∃ x; (!p(x) & !q(x)))
   6. (p -> ∀ x; q) <-> ∀ x; (p -> q)
   7. ((∀ x; R(x,x) & ∀ x, y, z; (R(x,z) & R(y,z))) -> R(x,y))) -> (∀ x, y; R(x,y) -> R(y,x))
   8. ((∀ x; R(x,x)) & (∀ x, y, z; (R(x,z) & R(y,z)) -> R(x,y))) -> (∀ x, y, z; (R(x,y) & R(y,z)) -> 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 of 1f 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

    /* 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() {
            // ...
        }
    }

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() {
        // ...
    }
}

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.

 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;

    // playfield
    /** 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();
    }

}

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.