Next: Correctness: Making software behave
Up: About Specware
Previous: About Specware
The software problem may be regarded as the result of our attempt to
build systems whose complexity exceeds our intellectual ability to
manage it.
Specware is a radically different effort to repair this
imbalance. Specware means to ensure that software
behaves as we need, to make software easier and faster to produce, to
increase the quality of the finished product, and to enable software
to evolve to match changing requirements and environments.
Specware is the embodiment of a formal method. Whereas most formal
methods have been devoted to the development of individual algorithms
and data structures, Specware is aimed toward the correct evolution
of entire systems. It achieves this advance by incorporating ideas
from the mathematical theory of categories as well as higher-order
mathematical logic. Through category theory, Specware unifies and
simplifies several seemingly disparate notions of software
engineering. In particular, Specware provides a conceptual and
notational basis for representing the composition of specifications
and their implementation as software components.
Whereas some formal methods have arisen as academic exercises, in
isolation from actual software practice, Specware has been developed
with the cooperation and encouragement of software practitioners from
industry and government, who use Specware every day for the
development of large software systems, whose correctness is critical.
Specware is the intellectual descendent of several widely applied
Kestrel synthesis tools, including KIDS, DTRE, and REACTO,
but it unifies and extends these tools.
Specware is motivated by the following analysis of the specific
causes of the software problem:
- The absence of a clear problem specification that reflects the
intentions of the software's designers without circumlocution or
paraphrase.
- The lack of an adequate mechanism for describing the
decomposition of a system's specification into more manageable
components.
- The absence of a means to express the relationship between a
problem's specification and its solution.
- The lack of a way to describe the evolution of a
problem, and its corresponding solution, over time.
Specware is designed to mitigate these problems.
Fundamental to Specware are the following notions:
- specification:
- A specification in Specware is identified
with a mathematical theory. Specifications can describe problems,
architectures, programs, data structures, and application domains.
- composition:
- The operation of composition in Specware
corresponds to the category-theoretic notion of a colimit. It
enables us to compose a specification from several simpler components
and to describe exactly how these components are related. (For
example, a specification for arrays of integers can be composed of
two component specifications, for arrays and integers.)
- refinement:
- Software development is accomplished in
Specware by refining one specification into another. Refinement
(also called interpretation) is a process in which all the
elements of one specification are represented in terms of another.
(For example, if a specification for lists is refined into a
specification for arrays, every operation on lists is described in
terms of operations on arrays.) Refinement can correspond to the
development of system architectures, the design of algorithms, and the
selection of data structures. Each refinement has an explicit
representation in Specware, an refinements can be manipulated by
the system. A complete refinement may be regarded as a history of the
system design process.
Software development in Specware is conducted in three stages.
- formation of a problem specification:
- Typically this is
accomplished by the composition of simpler specifications, many of
which may already exist in a specification library.
- refinement of the problem specification:
- Typically this is
achieved by successive refinement of the components of the problem
specification.
- code generation:
- When the problem specification has been
refined to a sufficiently low level, we can generate code in a desired
target language, such as LISP or, soon, C.
How does Specware achieve its goals? Let us examine each in turn.
Next: Correctness: Making software behave
Up: About Specware
Previous: About Specware
Richard Waldinger
Mon Jul 22 18:33:09 PDT 1996