|Testing, Debugging, and Verification||TDA567/DIT082, LP2, HT2015|
Exercises Week 5 - 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.
1. Loops and Invariants in DafnyThis 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. HashtableConsider 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:
3. Method loopWhat does the following method loop do, assuming that x is a positive integer? Add a specification and loop invariant for that method.
4. DivisionThe 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.
Exercise 5: 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 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.
You can define any predicate or function which you consider convenient .
|Home | Course | Schedule | Exam | Exercises | Labs | Evaluation | Tools | Links||Atze van der Ploeg, Dec 3, 2015|