[prev] 29 [next]

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 Sets in these terms.

Suggest an implementation for an  isValid()  function?