Testing, Debugging, and Verification TDA567/DIT082, LP2, HT2015
Exercises Week 4 - Formal Specification

These are the exercises for the exercise session in week 4. As for the second lab assignment, you will need to use Dafny.

Exercise 0: Getting Started with Dafny

Visit the Dafny Tutorial. Read sections 1-5 and do Excersises 0-6. You should try to do this at home.

Exercise 1: Counter

Consider the following class Counter. This class represents a simple counter. Methods inc and dec are used to increment and decrement the counter (i.e. variable value) respectively, method getValue returns the actual value of the counter, the constructor init is used to initialize Counter objects and variable value is always greater or equal than zero. Method Main is there only for testing purposes.

Your task is to add specifications for all the methods in the class. You can define any predicate or function which you consider convenient .

Solution

Exercise 2: Fix Size Lists

Consider the following partially implemented class List which represents fix size lists. On this class, method head returns the initial element of the list (i.e. the head of the list), method tail removes the head of the list, method snoc adds element at the end of the list, the variable size represents the total amount of values on the list and the constructor init is used to initialize List objects. On a list, values are stored on the array a. Method Main is there only for testing purposes.

  1. Your task is to add specifications for all the methods in the class. When doing this, take into account that:

    • size is greater or equal than zero and can be increased up to a.Length.
    • The array a cannot be null.
    • After calling constructor init there should be space for at least one element in the list.
    • If the size is strictly greater than zero, then all of the following must hold:
      • head returns the initial element of the list (i.e. the head of the list).
      • tail shifts all the elements in a one position to the left.
    • In snoc, size represents the index where the new element should be stored.

    You can define any predicate or function which you consider convenient .

  2. After writing all your specifications, were there any error? If so, was it on an assertion? Was it on a postcondition? Reflect about this.
Solution

Exercise 3: Tic Tac Toe

Tic tac toe is a game for two players where each player takes turns in order to fill in a 3x3 grid with Os and Xs (each player can only use one of these symbols). The first player who succeeds in placing three of his/her marks in a horizontal, vertical, or diagonal row wins the game.

Tic tac toe example

Consider the partially implemented class Tictactoe which represents a Tic tac toe game. This class represents the grid by using the array board. However, when fill in by using method PutValue, its coordinates are given in the usual two-dimentional way, i.e. by giving its coordinates x and y on the grid. Method BoardPosition is translating (x,y) coordinates into valid indexes of board.

Your task consists of adding specifications for all the methods in the class. When doing this, take into account that:

  • The array board cannot be null and its length is always 9.
  • Constructor Init is used to initialize Tictactoe objects.
  • For any index i, board[i] == 0 means empty entry, board[i] == 1 means O, board[i] == 2 means X.
Solution

Exercise 4: Quantifiers

Consider an array a with n integer elements. Let j and k be two indices, 0 <= j < k < n. In the questions below, by 'a[j..k]' we mean a segment of the array b including the elements at positions j and k.

Use the online for Dafny and write the following as Dafny assertions in this template file: Q1. Alternatively, use the file Question1.dfy. Save a copy when you are satisfied that your solutions are correct.

  1. All elements in a[j..k] are zero.
  2. All zeros of a[0..n-1] are in b[j..k].
  3. It is not the case that all ones of b[0..n-1] occur in the interval b[p..r].
    (Write this in two ways, once using negation ('!') and once avoiding negation.
  4. a[0..n-1] contains at least two zeros.
  5. 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 evaluate to true if b has only one element?)
Solution

Exercise 5: Simple Class

Your task is to complete the class Secret.dfy, and write specifications for its methods. Implement and write formal specifications for the methods Init and Guess. Check that your implementation and specification agree.

(A) The Init method initialises a new object of type Secret, by setting the secret to the values x. The value of x is required to be between 1 and 10. After initialisation, the field secret must hold the secret number, the number of guesses is 0 and the secret is not known. 

 method Init(x: int)
(B) The Guess method takes in a guess and returns two values, a boolean result which is true if the guess was correct and false otherwise, and an integer guesses telling how many guesses has been made so far. The precondiditon of the method is that the secret is still unknown. Each time the user make a guess, the count should be incremented. If the user guesses correctly, the secret becomes known, otherwise it remains unknown. 
method guess(g : int) returns (result : bool, guesses : int)
(C) Complete the Main method with some tests: Create an object, make some guesses and assert some properties about the expected results. Compile and check your code.

Solution



Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools | Links Atze van der Ploeg, Nov 27, 2015