1. Consider the (partial) Java classes Interval and IntervalSeq.
public class Interval f
private nal int start, end;
public Interval(int start, int end) f
this.start = start;
this.end = end;
g
public int getStart( ) f
return start;
g
public int getEnd( ) f
return end;
g
g
/** Class to represent sequence of intervals. */
public class IntervalSeq f
protected int size = 0;
protected Interval[ ] contents = new Interval[1000];
/** Insert a new element in the sequence. */
public void insert(Interval i) f
...
g
// more methods
g
In class IntervalSeq, the eld size holds the number of Interval objects which have been
inserted into the IntervalSeq object. All inserted Interval objects are stored in the beginning
of the array. The remaining cells of the array are null. Augment the classes with JML
speci cations, including assignable clauses where appropriate, stating that
(a) getEnd( ) is always greater than or equal to getStart( ) (2 marks)
(b) size is always less than or equal to contents:length and all elements of contents below
the position denoted by size are non-null. (2 marks)
(c) If size is strictly smaller than contents:length then the method call insert(i) terminates
with size increased by 1 and the interval i appearing at the end of the existing sequence
of intervals. (2 marks)
(d) If size has reached contents:length then insert will throw an IndexOutOfBoundsException.
(2 marks)
You do not need to write any code or use KeY for this question.
2. The following class ArrayCopy has utility methods for copying portions of integer arrays
from a source array src to a destination array dest. The top level method arrayCopy is
capable of copying data even within the same array (when src == dest) in which case the
data is rst copied from the source region to a temporary array and then from the temporary
array to the destination region. This way data corruption is avoided when the two regions
overlap. The private method copy works under the assumption that the provided arrays are
non-null and di erent by reference, and that all other data (o sets and number of elements
to be copied) are well de ned.
public class ArrayCopy f
public void arrayCopy( int[ ] src, int srcO set, int[ ] dest, int destO set, int numElems)
throws IllegalArgumentException f
if (src == nulljjdest == nulljjnumElems src.length jj destO set + numElems > dest.length) f
throw new IllegalArgumentException( );
g
if (src == dest) f
int[ ] temp = new int[numElems];
copy(src, srcO set, temp, 0, numElems);
copy(temp, 0, dest, destO set, numElems);
g else f
copy(src, srcO set, dest, destO set, numElems);
g
g
private void copy(int[ ] src, int srcO set, int[ ] dest, int destO set, int numElems) f
int i = 0;
while(i < numElems) f
dest[destO set + i] = src[srcO set + i];
i++;
g
g
g
(a) Provide a JML speci cation for the arrayCopy method. (5 marks)
(b) Provide a JML speci cation for the copy method. (3 marks)
(c) Provide a JML loop invariant, variant and assignable clause for the loop in the copy
method. (3 marks)
(d) Show that the code satis es your speci cations using KeY. Save the proof le for sub-
mission.
(1 mark)
3. This question is to be completed by CSSE7100 students only.
Consider the following interface and classes.
public interface A f
public int m();
g
public class B implements A f
//@ ensures nresult == 1;
public int m( ) f
return 1;
g
g
public class C implements A f
//@ ensures nresult == 2;
public int m( ) f
return 2;
g
g
public class D f
private /*@ nullable @*/ A[ ] a;
... // other methods
/*@ requires 0 <= i && i < a.length;
@ requires ninvariant for(a[i]);
@ ensures 0 <= nresult && nresult <= 2;
@*/
public int m(int i) f
if (a==null) return 0;
return a[i].m( );
g
g
(a) Explain why the method m in class D is incorrect. (1 mark)
(b) Provide one or more class invariants to make the method correct. (3 marks)
Marking
The assignment is worth 20% of your nal grade. Each question is worth the marks indicated
adding to a total of 20 marks (for CSSE3100 students) and 24 marks (for CSSE7100 students).
A mark of zero will be given for work with little or no academic merit.
Submission
This assignment is due on Friday 4 May, 5pm. The following should be submitted by Blackboard
by the due date and time.
A le assignment2.pdf containing your answers to Q1, Q2(a)-(c), and for CSSE7100 stu-
dents only, Q3.
A le ArrayCopy.proof containing your proof for Q2(d).
Late submission: Please see Section 5.3 of the Course Pro le regarding extensions to assignment
due dates.
School Policy on Student Misconduct
This assignment is to be completed individually. You are required to read and understand the