1. 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.

2. Specifying a sorting algorithm

Sortedness predicate

1a. Write a predicate sorted that takes a sequence of integers (seq<int>). The predicate should be true if and only if the sequence is sorted in increasing order.

1b. There are often many ways to express equivalent properties, but some work better than others for program verification. Write a second predicate sorted' that is equivalent, but uses a different definition.

Lemmas

You can write and prove lemmas to verify properties of your programs and predicates. Lemmas in Dafny are 'ghost methods', methods that are verified but not compiled. For example the following lemma SortedShortSequences can be read as follow: for all sequence a, if the size of a is less than 2, then a is sorted. When the lemma is simple enough, we can leave the body of the method empty, and Dafny can prove it automatically.

ghost method SortedShortSequences(a : seq<int>)
  requires |a| < 2
  ensures sorted(a)
{
}
              

2a. We want to show that our two definitions of sortedness are equivalent. Write one lemma that expresses the property if a sequence is sorted', then it is sorted and another that expresses the property if a sequence is sorted, then it is sorted'. Note: it is possible that Dafny does not manage to prove one of the lemmas. This does not necessarily mean that it is false, but simply too difficult to be proven without help. In this case, simply comment out the lemma to allow the verification to go through.

2b. Write a proof of your two lemmas on paper. Which of your two definitions is the most convenient to use?

Mystery predicate

3a. Explain the meaning of the predicate p below.

predicate p(a : seq<int>, b : seq<int>)
{
   multiset(a) == multiset(b)
}
              

3b. Define another predicate p' that is equivalent to p but does not use multisets. You may find it useful to define an auxiliary function.

Specifying the method

4a. Write a full specification for a method that takes an array<int> and sorts it in place. You don't have to write the full method, only its specification. Note: we have defined our properties on sequences (which are immutable objects) but the program should be defined on arrays. To convert an array t into a sequence, use the "slice" notation t[..]

4b. The specification that you wrote in (4a) should use the predicate p. If it doesn't, your contract is under-specified: not all programs that satisfy it are sorting algorithms. In order to illustrate this: take the under-specified contract (the specification in (4a) minus the part that uses the predicate p) and write a simple program that satisfies it. (optionally, write it and verify it in Dafny).

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 Danfy contracts. 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
                   |
                   |- LimitedStack.dfy 
                   |
                   |- Sorting/
                   | |- sorting.dfy
                   | |- Report.pdf/txt
                   |
                   |- Tokeneer/
                   | |- *.dfy
                   | |- Report.pdf/txt
                   |