What is Specware For?

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.

• Correctness: Making software behave as we mean it to
• Productivity: Making software faster and easier to produce
• Quality: Making better software
• Evolution: Meeting changing requirements and environment