Exercise 4: Set ADT Pre/Post-conditions
If x is a variable of type T , an ADT
- ptr(x) is the pointer stored in
x
- val(x) is the abstract value represented by
*x
- valid(T,x) indicates that
- the collection of values in
*x
satisfies all constraints on "correct" values of type T
- x' is an updated version of x (ptr(x') == ptr(x))
Consider the pre/post-conditions on Set s in these terms.
Suggest an implementation for an isValid() function?
|