Writing software in Metaslang, the specification and programming language used in Specware, brings many advantages. Along with the previously-mentioned possibilities for incremental development, you have the option to perform rigorous verification of the design and implementation of your code, leading to the a high level of assurance in the correctness of the final application.
Specware allows you to work directly with abstract concepts independently of implementation decisions. You can put off making implementation decisions by describing the problem domain in general terms, specifying only those properties you need for the task at hand.
In most languages, you can declare either everything about a function or nothing about it. That is, you can declare only its type, or its complete definition. In Specware you must declare the signature of an operation, but after that you have almost complete freedom in stating properties of the operation. You can declare nothing or anything about it. Any properties you have stated can be used for program transformation.
For example, you can describe how squaring distributes over multiplication:
axiom square_distributes_over_times is
fa(a, b) square(a * b) = square(a) * square(b) |
This property is not a complete definition of the squaring operation, but it is true. The truth of this axiom must be preserved as you refine the operation. However, unless you are going to generate code for square, you do not need to supply a complete definition.
The completeness of your definitions determines the extent to which you can generate code. A complete refinement must completely define the operations of the source theory in terms of the target theory. This guarantees that, if the target is implementable, the source is also implementable.
Specware performs inference using external theorem provers; the distribution includes SRI's SNARK theorem prover. External provers are connected to Specware through logic morphisms, which relate logics to each other.
You can apply external reasoning agents to refinements in different ways (although only verification is fully implemented in the current release of Specware).
Verification tests the correctness of a refinement. For example, you can prove that quicksort is a correct refinement of the sorting specification.
Simplification is a complexity-reducing refinement. For example, given appropriate axioms, you can rewrite 3*a+3*b to 3*(a+b).
Synthesis derives a refinement for a given specification by combining the domain theory with computational theory. For example, you can derive quicksort semi-automatically from the sorting specification as a solution to a sorting problem, if you describe exactly how the problem is a sorting problem.