Example: Collection

   The theory of collections, defined in the Specware Language Manual, describes collections of objects for which it is unspecified whether the order or the multiplicity of elements is significant. Thus, while we cannot prove that the collections col(X, Y),   col(Y, X), and col(X, X, Y) are the same, neither can we prove that they are distinct. Sets , sequences , and bags  are all extensions of the theory of collections.

The specification for the theory is as follows:

spec COLLECTION is 
  sorts E, Col

  const empty-col : Col
  op insert-col : E, Col -> Col
 
  constructors {empty-col, insert-col} construct Col

  theorem decomposition is
    (implies (not (equal c empty-col))
             (ex (e d)(equal c (insert-col e d))))
end-spec

 

Here empty-col  is the empty collection  and (insert-col e c)  is the operation that inserts a new element e into the collection c. The collection that we informally write as col(d, e) is denoted in the theory by the term

  (insert-col d (insert-col e empty-col))

Note that Specware adheres to the LISP convention that (p c) denotes the result of applying an operator p to an argument c; in mathematical notation the result would be denoted by p(c).

The theory has no explicit axioms but it does have a constructor set  consisting of two elements, empty-col and insert-col. Intuitively speaking, this means that every collection can be constructed by successively inserting elements into the empty collection. Formally, it coincides with an induction  axiom, which may be paraphrased as follows:

To show that a property p holds for every collection c, that is, that

  (fa (c : Col) (p c))

is true, it suffices to show two things:

Base Case. That p holds for the empty collection col(), that is,

   (p empty-col)

Inductive Step. If p holds for an arbitrary collection c it also holds for the result of inserting an element e into c; that is,

  (fa (e : E  c : Col)
    (implies (p c)  (p (insert-col e c))))

As we have mentioned, the induction principle is represented as a tactic. When faced with a theorem of form (fa (c : Col) (p c)), the user may direct the system to prove the above base case and inductive step instead.

Although the theory of collections has no explicit axioms, it does have implicit axioms  corresponding to the sort constructors. In particular, the specification introduces the binary operator insert-col,  which is implicitly a unary operator on a pair. Therefore the axiom list  will include those that define the function project  and the constructor  function <e c> for pairs, such as

  (fa (e : E, c : Col)
    (equal ((project 1) <e c>) e))

(Actually the axiom will be printed without the angle brackets < and > but they are there implicitly.) Because the Specware theorem prover allows operators with multiple arguments, these axioms will normally be redundant. Mechanisms are provided for omitting them.

The specification for collections includes an explicit theorem, the decomposition  theorem for collections, which says that every nonempty collection can be decomposed into the result of applying the insertion function to an element and another collection. In parsing the specification, the theorem prover will treat this formula as a conjecture and attempt to prove that it follows from the implicit axioms for collections, perhaps using the induction  tactic.