Although formulating a specification and refining it into a proposed implementation are themselves valuable exercises, to derive the full benefit of Specware we may then use the refinement to generate code in a selected target programming language. For this purpose we must refine the system's specification into a theory that describes the constructs of that language. Currently, such theories exist for LISP and, soon, C; theories for other languages are anticipated.
Our refinement of the theory of plane geometry into the theory of real numbers cannot be used as a basis for code generation, because there is no implementation for the entire theory of real numbers. Real numbers can be represented by sequences of digits but, in general, these sequences may be infinite and uncomputable. Instead, we need a refinement of plane geometry into a computable theory, such as the computable reals. Also we need to refine that theory into the theory of the target programming language.
Furthermore, to generate code, it is not enough merely to refine the
specification into the theory of the target programming language. For
a refinement to be suitable for code generation, it must be
constructive. In other words, every operation in the source
specification must ultimately be identified with a finite computation.
For example, in the theory of plane geometry, suppose our
specification defines a colinear relation between three points, 
,
, and 
, by saying that there exists a line segment that
contains all three points. That definition is correct, but it doesn't
describe a finite computation--it doesn't tell us how to find the line in
question.. We might try to cycle through all the line segments in the plane
and somehow test if the three points are on it, but that is a potentially
endless computation.
A constructive refinement of the plane geometry theory must identify the
colinear relation with a relation defined in a way that suggests a
method of computation. For instance, the relation might hold if the
slope from to is the same as the slope from to
:
or, equivalently:
This relation is computable in the target theory.
In general, nonconstructive definitions in the source specification, which do not suggest a computation, must be identified with constructive, and efficiently computable, definitions in the target theory. Once this is done, code generation is automatic.
Theories of target programming languages, and some component refinements, are built into the Specware library. Although constructing a full refinement for a system's problem specification requires thought and time, the routine details are automated. And of course the process provides the correctness guarantee that the generated code must satisfy the source specification.
Although the plane geometry example is artificial, it is representative of many common software engineering problems in which an abstraction is given a concrete representation. Sets are represented as lists which are, in turn, represented as arrays. In computational fluid dynamics, the surfaces of aircrafts are represented by rectangular grids which are, in turn, represented as arrays of points, i.e., arrays of triples of numbers. Although Specware does not choose these representations automatically, it manages complex configurations of representations and it guarantees their conceptual adequacy.