Other Atomic Constructors for Set

The specification of a set data type has a number of other interesting features which are worth exploring. Firstly, although we chose empty and add as the atomic constructors, other atomic constructors could be chosen. For example, the three constructors :

• empty : -> set
• { _ } : nat -> set
• _ U _ : set set -> set

form a collection of atomic constructors. The second operation takes a natural number n and produces the corresponding singleton set {n} while the third operation U is the familiar set union operation $\cup$. With this collection of atomic constructors, the mathematical set {1,5,3} is represented by the expression {1} U {5} U {3}. A sufficiently complete specification results by considering the outcomes of the operations is-in? and delete acting on these three atomic constructors. The corresponding axioms are

          is-in?(empty, n)  =  false
          is-in?({n1}, n2)  =  IF  n1 == n2  THEN  true  ELSE  false  ENDIF
        is-in?(s1 U s2, n)  =  is-in?(s1, n)  or  is-in?(s2, n)
          delete(empty, n)  =  empty
          delete({n1}, n2)  =  IF  n1 == n2  THEN  empty  ELSE  {n1}  ENDIF
        delete(s1 U s2, n)  =  delete(s1, n) U delete(s2, n)

where n, n1 $\in$ nat and s, s1, s2 $\in$ stack.

On a point of some subtlety, although this may appear at first sight to specify a set, it is unfortunately deficient with regards to the expected mathematical properties of a set in four respects !

1.

With reference to set union, the empty set ($\emptyset$) is an identity element, that is the empty set has the property :

• empty U s = s     and     s U empty = s

2.

The union operation is commutative :

• s1 U s2 = s2 U s1

3.

The union operation is associative :

• s1 U (s2 U s3) = (s1 U s2) U s3

4.

The union operation is idempotent :

• s U s = s

These results cannot be derived as a consequence of the six axioms given above and need to be added to the specification. The resulting specification with its eleven axioms is shown in Fig. 12.4 (version-3).

  

Figure 12.4: Algebraic specification of a set - version 3