A unit definition consists of a unit identifier and a unit term. The identifier identifies the unit and the term defines how the unit is constructed.
A project developed with Specware consists of a set of unit definitions, some of which may come from libraries. Units have unique identifiers within the project.
A unit identifier is a finite, non-empty sequence of word symbols (word symbols are defined in the Metaslang grammar). The sequence of word symbols is essentially a "path" in a tree: the units comprising a project are organized in a tree.
This provides a convenient and simple way to organize the units comprising a project. Libraries are subtrees of the whole tree. Parallel development of different parts of a project can be carried out in different subtrees that can be later put together without risk of naming clashes.
A unit term is text written in the Metaslang language. Metaslang features various ways to construct specs, morphisms, and all the other kinds of units. For instance, it is possible to construct a spec by explicitly listing its types, ops, and axioms. It is also possible to construct a spec by applying the colimit operation to a diagram of specs and morphisms.
A unit term may reference other units. For instance, a spec constructed by extending another one references the spec being extended.
References can be "SWPATH-based" or "relative". In either case they are resolved to full unit identifiers of units in the tree, according to simple rules explained later.