University of Virginia, Department of Computer Science CS201J: Engineering Software, Fall 2003

Notes: Tuseday 16 September 2003
 Assignments Due

Notes and Questions
StringSet Specification
public class StringSet
// OVERVIEW: StringSets are unbounded, mutable sets of
//     Strings.  A typical StringSet is { x1, ..., xn }
public StringSet ()
// EFFECTS: Initializes this to be empty: { }
public void insert (String s)
// MODIFIES: this
// EFFECTS: Adds x to the elements of this:
//       this_post = this_pre U { s }
public boolean isIn (String s) {
// EFFECTS: Returns true iff s is an element of this.
//       \result = s elementof this
public int size ()
// EFFECTS: Returns the number of elements in this.

Representation Invariant

The Representation Invariant expresses properties all legitimate objects of the ADT must satisfy. It is a function from concrete representation to boolean:

I: C → boolean

To check correctness we assume all objects passed in to a procedure satisfy the invariant and prove all objects satisfy the invariant before leaving the implementation code.

public class StringSet {
// OVERVIEW: StringSets are unbounded, mutable sets of Strings.
//    A typical StringSet is {x1, ..., xn}

// Representation:
private Vector rep;

// RepInvariant (c) = c.rep contains no duplicates && c.rep != null
//                        && all elements of c.rep are of non-null Strings

//@invariant rep != null
//@invariant rep.containsNull == false
//@invariant rep.elementType == \type(String)
Abstraction Function

The Abstraction Function maps a concrete state to an abstract state:

AF: CA
It is a function from concrete representation to the abstract notation introduced in overview specification.
// AF (c) = { AFString (c.els[i]) | 0 <= i < c.els.size () }
Correctness of Insert
public void insert (String s) {
// MODIFIES: this
// EFFECTS: Adds s to the elements of this:
//     this_post = this_pre U { s }
if (!isIn (s)) { rep.add (s); }
}
Path 1: isIn (s)
If isIn (s) returns true, we know from the postcondition of isIn that s is an element of this_pre.

Since we take the else branch, we know rep is not modified by insert: rep_post = rep_pre. Thus, AF(rep_post) = AF(rep_pre) and this_post = this_pre since this_pre = AF(rep_pre) and this_post = AF(rep_post).

From set theory, we know if e is an element of x then x U e = x.

Hence, this_post = this_pre U s.

Path 2: !isIn (s)
If isIn (s) returns false, we know from the postcondition of isInt that s is not an element of this_pre.

On the true branch, we do { rep.add (s); }. We need to know what java.util.Vector.add does to understand how this effects the value of rep. Here's its spec:

// Modifies: this
// Effects: Appends o to the end of this.
//      this_post.size = this_pre.size + 1
//      this_post[i] = this_pre[i] forall 0 <= i < this_pre.size
//	    this_post[this_pre.size] = o
So, substituting rep for this for the method call, we have:
rep_post.size == rep_pre.size + 1
rep_post[i] = rep_pre[i] forall 0 <= i < rep_pre.size
rep_post[rep_pre.size] = s
We can substitute the value of rep_post into the abstraction function:
AF (rep_post) = { AFString (rep_post[i]) | 0 <= i < rep_post.size }
= { rep_post, rep_post, ...,  rep_post[rep_post.size - 1] }
= { rep_pre, rep_pre, ..., rep_pre[rep_post.size - 1], s }
= AF (rep_pre) U { s }
Hence, this_post = this_pre U { s }.
Since the specification is satisfied along all possible paths through insert, we have shown that insert satisfies its specification.