Testing, Debugging, and Verification TDA567/DIT082, LP2, HT2017
Exercises Week 6 - Formal Specification: Introduction to loops, invariants and Variants

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

You may find it useful to refer to the Dafny tutorial and the TDV Dafny FAQ

1. Loops and Invariants in Dafny

This week, we will work through the second half of the Dafny tutorial. Visit the Dafny Tutorial. Read sections 5-11 and do the associated exercises.

2. Hashtable

Consider the following class Hashtable. This class represents an open addressing hash table with linear probing as collision resolution. Within a hash table, values (of type int) are stored into a fixed array hashtable. Besides, in order to have an easy way of checking whether or not the capacity of hashtable is reached (i.e. the array hashtable is full), a field size keeps track of the number of stored objects and a field capacity represents the total amount of objects that can be added to the hash table.

The method add, which is used to add values to the hash table, first tries to put the corresponding value at the position of the computed hash code. However, if that index is occupied, then add searches upwards (modulo the array length) for the nearest following index which is free. A position is considered free if and only if it contains a 0.

Add specifications and loop invariants (if necessary) for all the methods and predicates in the class taking into account that:

  • The size field is never negative, and always less or equal than capacity.
  • The capacity should be the same value as hashtable.Length.
  • The array hashtable cannot be null.
  • There should be space for at least one element in the hash table.
  • The number of elements stored in array hashtable (i.e., the number of array cells whose content is not 0) is size.
  • The values added in hashtable are always positive (i.e. bigger than 0).
  • If the size is strictly smaller than capacity, then all of the following must hold:
    • add increases size by one.
    • After add(val,key), val is stored in hashtable at some valid index.
Download a solution here: Hashtable_sol.dfy

3. Method loop

What does the following method loop do, assuming that x is a positive integer? Add a specification and loop invariant for that method.
Download a solution here: Question3_sol.dfy

4. Division

The following method Division divides x by y. q contains the quotient afterwards and r the remainder. Find a loop invariant and a specification which verify the previous implementation.
Download a solution here: Division_sol.dfy

Exercise 5: 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 cons adds an element in the beginning 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 and loop invariants (if necessary) 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 smaller than a.Length, then all of the following must hold:
      • cons shifts all the elements in a one position to the right and then adds the new value in the position zero o a.
    • 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 .

Download a solution here: List_sol.dfy


Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools | Links Srinivas Pinisetty, Dec 15, 2017