The correctness issue is of primary concern to Specware adopters. But why should software constructed via this route be more likely to be correct than conventionally produced software?
Most obviously, Specware allows us to express our requirements in a formal specification. The specification can describe the desired behavior of the program independently of such implementation concerns as architectures, algorithms, data structures, and efficiency. The Specware language, based on logical notions, is also independent of the ultimate target implementation language. It is almost universally agreed that, even in the absence of software tools, the discipline of formulating specifications is crucial to the correctness and reliability of large software systems.
Of course, even though the specification describes behavior and function rather than architecture and implementation, there is no reason to assume that the specification is correct--in fact, first drafts of specifications for even simple programs are often wrong. (For example, early published specifications for sorting programs stated that the output must be in increasing order, but often neglected to mention that the output must be a permutation of the input; thus a program that produced any increasing output would satisfy the specification.)
Unfortunately, there is no formal technique that can guarantee that the specification correctly reflects the intentions of the software designer--to do that, it would be necessary to read minds. But Specware does provide tools to aid the user in formulating a specification and ensuring its correctness. We can use the inferential capabilities of Specware to establish that the specified system must have certain intended and desired properties. We may state the expected result of executing the system for sample inputs and situations, or we may assert other properties that are intended but are not already part of the specification. (For example, we may state that applying a sort program twice in succession to the same input yields the same result as applying it once--that is, sorting is ``idempotent.'') Establishing such properties doesn't prove that the specified program behaves as intended in all respects. However, if the specification fails to imply one of these properties, we cannot expect the implemented system to satisfy it. This tells us that something in the specification--or in the property--is wrong.
Another fact that encourages correctness in specification is that the user of Specware does not need to build specifications from scratch. Specifications are composed from other simpler specifications whose correctness is already established; these may be obtained from a specification library. The Specware system comes equipped with a basic specification library.
Finally, the processes of refinement and code generation will uncover certain specification errors, such as inconsistency. To generate code, we must refine our problem specification into a much lower level specification that describes the target language. The notion of refinement is defined so that any specification that we can refine into a consistent specification must itself be consistent. Therefore, the problem specification must be consistent, provided that the target language specification is.
The Specware implementation ensures that refinements of the initial specification satisfy the problem statement. Formation of a refinement involves proving the validity of certain applicability conditions, which is performed automatically by a theorem prover built into the Specware system. Failure to verify a condition indicates a potential implementation or specification error. Conversely, succesful verification of the conditions establishes the correctness of the implementation.