1. Property-based testing LLHashTable

In this lab you will be testing an implementation of a hash table which uses separate chaining with linked lists (see Wikipedia for more information on hash tables).

We use a property-based testing approach, much similar to what we did in the exercise session testing LimitedStack. As a brief recap, we base our approach on this article by Claessen and Hughes. The main idea is that we test that different operations on the class under test result in the same observable behaviour. To generate many cases for each test, we randomize the values used for each operation as well as the actions performed before and after these operations. In pseudo code, we test:

prefix = randomActions();
suffix = randomActions();

TestObject T1 = new TestObject();
TestObject T2 = new TestObject();

output1 = perform(T1, prefix) + perform(T1, command1) + perform(T1, suffix);
output2 = perform(T2, prefix) + perform(T2, command2) + perform(T2, suffix);

equals(T1, T2) && equals(output1, output2);

The output allows us to test methods that do not change the state of the class under test, such as get-methods. The testing framework handles most of this test, you only need to write the code that generates command1 and command2, i.e. the commands thats should be equivalent. For more information on the testing framework, see this page.

You can download this archive, which contains a number of files used by the testing framework. In this lab, you only need to concern yourself with the classes LLHashTable (the class under test) and LLHashTableTestSuite (where you should write your tests).

After familarizing yourself with the LLHashTable interface, get the test suite running. Most tests do not implement the desired properties and compare that "doing nothing" gives two observable equivalent hash tables. In combination with the actions added by the testing framework as prefix and suffix, this is the same as testing random sequences of actions. The only implemented test is thus commutePut.

Your task: Run the test suite and implement additional tests. Describe for each test which property it tests. E.g. for the example test, the property is:

• put(Ka,Va), put(Kb,Vb) <==> put(Kb,Vb), put(Ka, Va) iff Ka != Kb

As part of your submission, include the implemented tests, document the bugs that you found and with which test, and how you fixed each bug.

2. Specifying LimitedStack

Consider the class LimitedStack. A LimitedStack object represent a Stack data-structure, that is a queue following the last-in-first-out principle. In addition, it can only hold a maximum number of elements, given by the field capacity. The stack itself is represented by an array of this length. The current top of the stack is located at index top. If the stack is empty, top is -1.

Now, the above is not very precise, so your job is to formally specify and implement the methods listed below.

            class LimitedStack {

                 var arr : array;    // contents
                 var capacity : int;   // max number of elements in stack.
                 var top : int;       // The index of the top of the stack, or -1 if the stack is empty.


                method Init(c : int)
                . . .
                {
                 capacity := c;
                 arr := new int[c];
                 top := -1;
                } 
                . . . 
            }
            

> LimitedStack.dfy (uncomment the function-headers as you work through the assignment.)

a.Useful Predicates

First of all, specify a predicate Valid, which specifies the properties and values allowed for fields of objects belonging to the LimitedStack class. You will need Valid in the specifications of the other methods. Valid should specify the following relationships:

• arr is not null
• The capacity must be positive, so we can put at least something on the stack.
• The capacity and the length of arr must agree.
• top should be at least -1 and strictly less than capacity.

Hint: Remember to specify the reads clause for each predicate!

b. The Init method

Recall that Dafny initialises object by an Init method. Complete its specification, making use of the invariant and predicates from part A as appropriate:

• The initial capacity of the stack, given by the input parameter c must be greater than 0. Consequently, the size of the newly created array arr should indeed be c.
• Newly created stacks are always empty.

c. isEmpty, Peek, Push and Pop

Now write down specifications for the methods isEmpty, Peek, Push and Pop. Then implement them, and make sure the implementation satisfies the specification.

• isEmpty should return true if and only if the stack is empty.
• Peek should return the top element of the stack, without removing it.
• Pop should remove the top element of the stack and return it.
• Push should push an element onto the top of the stack, provided that the stack is not already full.

d. A second version of Push

Now, also specify and implement a second version of push, called Push2. This functions differ from the standard implementation of push from part C in the following ways:

• It can be called whether or not the stack is full.
• If the stack is full, the oldest element should be dropped to make space. Use the helper method Shift to do this, without modifying it or its specification.
• If the stack is not full, the previous elements should be kept as usual.
• Your specification must describe those two bevahiours and how they depend on the initial state of the stack. You can use predicates inside old too.

e. Assertions and Testing

Ensure that Dafny can prove that the tests and assertions in the Main method hold. If not, go back and study your specifications and implementations. Remember that the Dafny verifier cannot see the code inside the method bodies (as opposed to functions or predicates), but only specification pre- and post-conditions.

3. A mini version of Tokeneer

While the real system has a very large specification, this question asks you to model a high-level mini-version of the Tokeneer system in Dafny and verify its correctness. The picture below shows the secure door system you are to model and verify. To enter the door, the user first needs to enrol and receive a token, which stores fingerprint data (for simplicity, you may assume fingerprints are represented by integers) and the security clearance level (there are three clearance levels: Low, Medium and High). The enrolment station keeps track of the users in the system to make sure no one can be issued with more than one token at the time.

When a user wants to open a door, the ID station checks that the user's fingerprint agrees with what is stored on the user's token and that the user have the adequate security clearance to enter this door. If a security breach is discovered, i.e. a token is used by the wrong person, this token must be invalidated immediately and the alarm sound.

As you no doubt notice, the above description in English is not as exact and precise as in Question Your task is to write a formal specification for the above system, and then implement it as a Dafny program, checking that your implementation satisfies your specification. In addition to your Dafny source code, you will also submit a brief report motivating your decisions and specifications (at most one page of A4).

The components of the system

Design the classes representing the different elements of the system:

• Tokens delivered to users. Tokens must store their user's identifier and a security clearance. Tokens may be invalidated.
• ID stations corresponding to a certain door, with a given security level. The state of the door and the alarm can be simply represented by booleans.
• The enrollment station, which must keep track of the user who currently have a token

The actions

For each of those actions, start by describing in English, briefly but precisely, the associated pre-conditions and post-conditions. In certains, cases, the post-conditions can depend on the input (e.g. "if the token is still valid ..., otherwise ..."). Then translate those requirements to methods and their contratcs in Dafny. Don't forget the modifies clause.

• Treating the demand of a user attempting to open a door. The users must provide their identity and a token.
• Closing a door
• Issuing a new token for a specific user and security level
• Invalidating a token

Implementation and test

Complete your methods by giving their implementation. You may realize that you need to modify the contracts, but think carefully if you do! Finally, add a test program exploring the different cases. Use assertions to check that Dafny is able to verify the expected properties of the program.

                  LAB2.zip
                   |
                   |- LLHashTable.java
                   |- LLHashTableTestSuite.java
                   |- LLHashTableReport.txt
                   |
                   |- LimitedStack.dfy 
                   |
                   |- Tokeneer/
                   | |- *.dfy
                   | |- Report.pdf
                   |