1. Specifying SortedIntegers

Consider the class SortedIntegers, which is similar to the class shown in the lecture. A SortedIntegers object can potentially contain duplicate integer elements.

Note that the array arr must be sorted all the time, and the implementations of the various methods will rely on that.

            public class SortedIntegers {

                private int arr[];

                private int capacity, size = 0;

                public SortedIntegers(int capacity) {
                    this.capacity = capacity;
                    this.arr = new int[capacity];
                }

                public void add(int elem) {
                    // ...
                }
                
                public void remove(int elem) {
                    // ...
                }
                
                public boolean contains(int elem) {
                    // ...
                }

                public int max() {
                    // ...
                }

                public int getSize() {
                    // ...
                }

                public int getCapacity() {
                    // ...
                }

                public String toString() {
                    // ...
                }
            }
            

> SortedIntegers.java

a. Specification of SortedIntegers

Specify all the methods in SortedIntegers (except toString()) using JML, taking advantage of invariants where possible.

b. Invariants

• Did you use invariants in your specification? If you did not, go back to the previous point and specify using invariants.
• Explain in the report why it is useful to use invariants; in explaining it, give a concrete example using the method specification of add or remove.

c. Implementation of SortedIntegers

Implement the methods in SortedIntegers. The implementation must fully comply with the specification.

2. Finding Duplicates

Take a look at the following Java code; a method that finds duplicate elements in an array of strings.

            public class FindDuplicate {

                public static void main (String[] args) {
                    System.out.println(findDuplicate(args));
                }

                public static String findDuplicate(String[] arr) {

                    HashTable tab = new HashTable(100);

                    for (int i = 0; i < arr.length; i++) {
                        if (tab.contains(arr[i]))
                            return arr[i];
                        tab.add( arr[i] );
                     }
                     
                     return null;
                }
                
            }
            

> FindDuplicate.java

The code uses a class HashTable that we will keep abstract for now.

a. Specifying FindDuplicate

Specify the intended pre- and post-condition of the method findDuplicate() using JML.

b. Specifying HashTable

Here is the signature of a Java class for a simple hashtable:

              public class HashTable {
                  ...

                  public HashTable(int init) {
                    ...
                  }

                  public int getSize() {
                    ...
                  }

                  public void add(Object x) {
                    ...
                  }

                  public boolean contains(Object x) {
                    ...
                  }

                  public void remove(Object x) {
                    ...
                  }
                
              }
            

Here is how we could implement the hash-table, using an open-addressed hash-table implementation. We use an array of linked lists, implemented by the local class EntryList.

              public class HashTable {

                  EntryList[] arr;
                  int size;
                
                  /* A simple linked list of entries. */
                  private class EntryList {
                       Object first;
                       EntryList rest;

                       EntryList(Object first, EntryList rest) {
                           this.first = first;
                           this.rest = rest;
                       }
                   }
                
                  /* Creates an empty hashtable with an array of length init. */
                  public HashTable(int init) {
                      arr = new EntryList[init];
                      size = 0;
                  }

                  ...
            

> HashTable.java.

The following properties should be expressed in JML.

1. Specify the invariant(s) of this class. Do not forget to express the following information:
   • Each object lies in the correct linked list.
   • No object can appear twice in the table.
2. Specify the method getSize.
3. Specify the method contains.
4. Specify the method add.
5. Specify the method remove.

Hint: Consider inventing a pure helper method contains in EntryList, which you can use in the other specifications. EntryList::contains must also be specified of course. The exercise session on Tuesday will be a good preparation for specifying EntryList::contains.

                  LAB2.zip
                   |
                   |-ex1
                   | \- SortedIntegers.java 
                   |
                   |-ex2
                   | |- HashTable.java
                   | \- FindDuplicate.java
                   |
                   \-report.txt