The first step in building an application in Specware is to describe the problem domain in abstract form. You use the Metaslang language to build specifications (specs) that describe the abstract concepts of the problem domain. Specs contain types, which denote collections of values, operations, which denote functions on values, and axioms, which describe the required properties of the operations in logical formulas.
To design specifications, you may combine top-down and bottom-up approaches. To begin, you break down the problem domain into small, manageable parts that you can understand more easily in complete detail. You create specifications for each part. This conceptual decomposition process allows you to isolate and describe each detail of functionality.
You then extend and compose the smaller specifications to form a larger, more complex specification.
You create morphisms to describe how specifications are related. A morphism is a formal mapping between two specifications that describes exactly how one is translated or extended into the other. Morphisms can describe "part-of" as well as "is-a" relationships.
You can extend a specification by importing it and adding new concepts. When you extend a specification, you can also translate the names of the concepts to a different terminology.
As you extend the specification, you provide more and more information about the structure and details of the types and operations, by including axioms and theorems to describe them.
You compose simple specifications to form more complex specifications using substitutions (e.g., to instantiate parameterized specifications) and colimit. Colimit "glues" specs together along shared concepts. Morphisms describe exactly how concepts are shared.
When you have described the abstract concepts in your problem domain, you begin the refinement process. Refinement maps a problem specification set into a solution specification set. Refinements replace functionality constraints with algorithms and abstract types with implementation data structures. You refine a specification by mapping it into the implementation domain. You describe how the concepts of the problem domain are implemented in terms of computational concepts. Computational concepts, such as numbers (e.g., integers) and collections (e.g., lists) are already specified in the Specware library. In the process of refinement, you build a bridge from your abstract specifications to these concrete, implementation-specific specifications.
Morphisms are also used to describe how each specification is to be mapped into a desired target specification. The source spec is a more abstract description of concepts, while the target spec describes those concepts more concretely. Often, the target spec is obtained by extending some other spec that contains concepts in term of which the concepts of the source spec are expressed. For example, if you have an abstract spec for a house, you can refine it by importing a spec for materials (wood, etc.) and expressing how the house is built in terms of those materials.
A morphism maps each type or operation of the source spec to a type or operation of the target spec. In certain cases, it may be useful to map a type or operation to a new type or operation that is not present in the target spec but that is defined in terms of those in the target spec. Interpretations are used for this purpose.
An interpretation contains three specs: a source spec (the domain), a target spec (the codomain), and a mediator. The mediator spec extends the target, so there is an inclusion morphism from the target to the mediator. A morphism from the source spec to the mediator expresses how the source spec maps to the extension of the target spec.
A morphisms can be viewed as a particular kind of interpretation where the mediator coincides with the target. Indeed, the refinement relation between a more abstract spec and a more concrete one can be expressed by a morphism but also by an interpretation.
You build up a refinement in the same way you build up a specification, in an iterative, stepwise progression. You build basic morphisms (or interpretations) from more abstract specs to more concrete specs, then compose the morphisms to extend the refinement. There are two ways to compose morphisms.
Sequential composition (A=>B + B=>C = A=>C) deepens a refinement. For example, if you are specifying a house, you might use sequential composition of morphisms to create an increasingly detailed description of a single room.
Parallel composition (A=>A' + B=>B' = (A,B) => (A',B')) widens, or increases the complexity of a refinement. For example, in the specification of a house, when you have several morphisms that refine different rooms, you could combine them in parallel to create a description of a multi-room house. You could do this before or after providing the additional detail for each one. You use the colimit method for this kind of composition, as you do to compose specifications.
Specware contains a library of specs that fully describe various mathematical and computational concepts that you need to produce an implementation of an abstract specification. The goal of refinement is to refine your abstract specs in terms of these library specs. This process guarantees that Specware can generate code to implement your specifications in its target language, Lisp.
Once the abstract spec is refined to a "constructive" spec, Specware can generate code in the target language. The generated code contains a function for each of the operations you have described in the abstract specification. After you examine and test it, you can embed it in an application that uses the functions.