The theory of sacks , defined in the Specware\ Language Manual, describes collections of object in which the order of elements is insignificant, but it is unspecified whether the multiplicity of elements is significant. Thus, we can prove that sack(X, Y) and sack(Y, X) are the same but we cannot prove whether sack(X, Y) or sack(X, X, Y) are the same or distinct. Maybe so, maybe not. Sets and bags are extensions of the theory of sacks, but sequences are not, because the order of the elements of a sequence is certainly significant.
The specification for the theory is as follows:
spec SACK is
import
translate COLLECTION
by {Col -> Sack,
empty-col -> empty-sack,
insert-col -> insert-sack}
op in-sack? : E, Sack -> Boolean
axiom empty is
(not (in-sack? e empty-sack))
axiom in-sack is
(iff
(in-sack? e (insert-sack d s))
(or (equal e d)
(in-sack? e s)))
axiom exchange is
(equal
(insert-sack e (insert-sack d s))
(insert-sack d (insert-sack e s)))
theorem retention is
(in-sack? e (insert-sack e s))
theorem conservation is
(not (equal empty-sack (insert-sack e s)))
end-spec
The theory of sacks imports the theory of collections, translated to reflect a change in vocabulary, such as empty-sack instead of empty-col. Thus the axioms for the theory of sacks will include the axioms for the theory of collections, translated in the same way. The induction tactic for sacks will be translated into an induction tactic for collections.
In addition, the theory of sacks introduces its own axioms, including those that define the membership function in-sack? and one, the exchange axiom, that conveys the fact that order is irrelevant in a sack. There are also some implicit sort axioms. All these are included in the axiom list .
The specification includes two explicit theorems, the retention and conservation theorems, which give properties of the membership function for sacks. Specware will regard these as conjectures and attempt to prove that they follow from the list of axioms.