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 DafnyVisit the Dafny Tutorial. Read sections 1-5 and do Excersises 0-6. You should try to do this at home.Exercise 1: CounterConsider 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 .
Exercise 2: Fix Size ListsConsider 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.
Exercise 3: Tic Tac ToeTic 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.
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:
Exercise 4: QuantifiersConsider 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.
Exercise 5: Simple ClassYour 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. | |
Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools | Links | Atze van der Ploeg, Nov 27, 2015 |