Assignment: Dafny and VeriFast
Dafny
A binary min-heap without duplicated elements is a binary tree which satisfies two properties:
1. the value of each node is (strictly) greater then the value of its parent, with the minimum-value element at the root (this is the min-heap property), and
2. is complete.
Binary heaps have efficient implementations on arrays. There are logarithmic algorithms to insert an element in a heap and to remove the minimum element from an heap. We concentrate on the former.
Consider the below class featuring a partial implementation of a binary min-heap. The root is the second item in the array. We skip the index zero cell of the array for the convenience of implementation.
class Heap {
var size : nat ;
var heap: array < i n t > ; method insert (x : int ) requires minHeap ( )
ensures minHeap ( )
{
/ / Insert the new item at the end of the array
var pos := s i z e + 1 ;
/ / P e r c o l a t e up
while pos > 1 && x < heap [ pos / 2 ] { heap [ pos ] := heap [ pos / 2 ] ;
pos := pos / 2 ;
}
heap [ pos ] := x ;
}
}
Write predicate minHeap() and add the necessary contract and annotations to method insert () so that Dafny accepts the code. In method insert, assume that there is enough room in the heap array to contain the new element.
Suggestion: proceed in two steps.
1. Start with the quasi binary heap property.
2. Once this is working proceed to show that the complete binary tree property is preserved by method insert () .
VeriFast
Modern lists come equipped with a selection mechanism. Would you like to keep track of your favourite tunes? A SelectionList is what you need! Given a list of tunes, all you have to do is to mark your favourite tunes and then extract these to a new list.
To make things simpler we will not allow duplicates, neither in the entries nor in the marks. We are interested in a Java class SelectionList with the following methods.
SelectionList () Builds an empty selection list, that is, a selection list with no entries or marks.
boolean contains(Object e) Returns true when object e is one of the entries in the selection list, and false otherwise. Both the entries and the marks are kept unchanged.
void add(Object e) Adds an element to the entries in the list. The operation has no effect when object e is an entry in the list. Marks are kept unchanged.
void mark(Object e) In order to mark an element, the element must be one of the entries in the list. The operation has no effect when object e is a mark in the list. Entries are kept unchanged.
void resetMarks() Clears all marks in the list; leaves the entries unchanged.
int size () Returns the number of entries in the list. Both the entries and the marks are kept unchanged.
SelectionList extract () Returns a selection list containing as entries the marks in the original list, and no marks. Both the entries and the marks in the original selection list are kept unchanged.
Use reference equality (==) to compare both entries and marks. Select an appropriate representation for your class. Write a predicate to specify the observable behaviour of a class without exposing its internal representation.
Add pre and postconditions to all your methods defining the contracts detailed above. Make sure your code compiles with the Java compiler (as well as it passes the VeriFast verifier).
Suggestion: Work at one method at a time, by adding gradually adding contracts to your methods. Leave method extract to the end.
Format your assignment according to the following formatting requirements:
1. The answer should be typed, double spaced, using Times New Roman font (size 12), with one-inch margins on all sides.
2. The response also include a cover page containing the title of the assignment, the student's name, the course title, and the date. The cover page is not included in the required page length.
3. Also Include a reference page. The Citations and references should follow APA format. The reference page is not included in the required page length.