Description
Part 2: Design by Contract
Posted on Piazza:Resources Assignments is a zip file CFJ_BST_Iter.zip. Unzip this file
to obtain a directory CFJ_BST_Iter containing a fully configured project which you may import into
Eclipse by doing: File Import Existing Projects into Workspace. The added configurations permit
the inclusion of CoFoJa contract annotations in the Java source.
The imported project contains a file BST_Contract.java with the familiar Tree and DupTree
classes along with a class BST_Iterator which works on both trees and duptrees. The class
DupTree extends Tree and the values in both types of trees are integers. Also included is an
@Invariant(ordered()) clause for class Tree.
Your task in this part of the assignment is to write CoFoJa contracts (@Requires and @Ensures
annotations) for the constructor of BST_Iterator and the two methods that modify its state,
namely, next() and stack_left_spine().
Writing Contracts. The contracts should capture the basic requirements and properties of the
iterator, namely, that:
1. the iterator only works on binary search trees;
2. the values are returned in ascending order; and
3. the stack invariant (described in Lecture 9) is maintained.
Your contracts may refer to the fields count, value and stack of BST_Iterator as well as
functions that do not modify the state of any object, such as Tree.min(), Tree.max(),
Tree.ordered(), Stack.isEmpty(), Stack.peek(), BST_Iterator.hasNext(), etc.
Running the Program. In order to run your program, you need to give the name of the .jar file in the
VM Arguments of the Run Configuration, as follows:
-javaagent:lib/cofoja+asm-1.3.1-20170424.jar
Run BST_Contract.java augmented with contracts and ensure that the program works correctly.
What to Submit. Prepare a top-level directory named A5_Part2_UBITId1_UBITId2 if the assignment is
done by a team of two students; otherwise, name it as A5_Part2_UBITId if the assignment is done
solo. (Order the UBITIds in alphabetic order, in the former case.) In this directory, place the
directory BST_CFJ containing the revised BST_Contract.java augmented with contracts.
Compress the top-level directory and submit the compressed file using the submit_cse522
command. Only one submission per team is required.
End of Assignment 5 – Part 2
