We have mentioned that, in Specware, a specification corresponds to a mathematical theory and can describe a problem, an architecture, a data structure, a program, or an entire application domain. Specifications describe the vocabulary of the theory and its properties. The vocabulary gives names to the entities in the theory; the properties are facts that are true of those entities.
For instance, to formulate a Specware theory of plane geometry, we will want to introduce specifications for the object of the theory. We may have a specification POINT for points, SEGMENT for line segments, ANGLE for angles, and QUAD for quadrilaterals. The vocabulary of SEGMENT will include the term ``endpoint'' to refer to the points at the end of the line segment; it will also provide the term ``perpendicular'' to describe a relation between two line segments. The vocabulary of QUAD may provide names for the four sides of the quadrilateral.
The meanings of the terms in the vocabulary of a specification are established by providing axioms, logical sentences that hold for the objects in the theory. For instance, an axiom for the perpendicular relation in SEGMENT might say that if a line segments x and y are perpendicular, then y and x are also perpendicular. The axioms for QUAD might say that adjacent sides of the quadrilateral share adjoining endpoints. The properties of a specification are all the logical sentences implied by its axioms.
Specifications are not independent; typically more complex specifications are built from simpler ones. The specification SEGMENT will be built from the specification POINT. When one specification is build on another, it inherits all the properties of the simpler one, and may have additional axioms of its own. For example, the specification RECT for a rectangle will be built from QUAD, and will contain the additional axiom that adjacent sides are perpendicular.
We now want to illustrate two fundamental ideas of Specware, the colimit and refinement.