Conceptually, there are two major stages in producing a Specware application. In the actual process, steps from these two stages may alternate.
Building a specification
Refining your specifications to constructive specifications
You must build a specification that describes your domain theory in rigorous terms. To do this, you first create small specifications for basic, abstract concepts, then specialize and combine these to make them more concrete and complex.
To relate concepts to each other in Specware, you use specification morphisms. A specification morphism shows how one concept is a specialization or part of another. For example, the concept "fast car" specializes both "car" and "fast thing". The concept "room" is part of the concept "house". You can specialize "room" in different ways, one for each room of the house.
You specialize in order to derive a more concrete specification from a more abstract specification. Because the specialization relation is transitive (if A specializes B and B specializes C, then A specializes C as well), you can combine a series of morphisms to achieve a step-wise refinement of abstract specifications into increasingly concrete ones.
You combine specifications in order to construct a more complex concept from a collection of simpler parts. In general, you increase the complexity of a specification by adding more structural detail.
Specware helps you to handle complexity and scale by providing composition operators that take small specifications and combine them in a rigorous way to produce a complex specification that retains the logic of its parts. Specware provides several techniques for combining specifications, that can be used in combination:
The import operation allows you to include earlier specifications in a later one.
The translate operation allows you to rename the parts of a specification.
The colimit operation glues concepts together into a shared union along shared subconcepts.
A shared union specification combines specializations of a concept. For example, if you combine "red car" with "fast car" sharing the concept "car", you obtain the shared union "fast, red car". If you combine them sharing nothing, you obtain "red car and fast car", which is two cars rather than one. Both choices are available.
You combine specifications to extend the refinement iteratively. The goal is to create a refinement between the abstract specification of your problem domain and a concrete implementation of the problem solution in terms of types and operations that ultimately are defined in the Specware libraries of mathematical and computational theories.
For example, suppose you want to create a specification for a card game. An abstract specification of a card game would include concepts such as card, suit, and hand. A refinement for this specification might map cards to natural numbers and hands to lists containing natural numbers.
The Specware libraries contains constructive specifications for various types, including natural numbers and lists.
To refine your abstract specification, you build a refinement between the abstract Hand specification and the List-based specification. When all types and operations are refined to concrete library-defined types and operations, the Specware system can generate code from the specification.