Specware is designed with the idea that large and complex problems can be specified by combining small and simple specifications, and that problem specifications can be refined into a working system by the controlled stepwise introduction of implementation design decisions, in such a way that the refined specifications and ultimately the working code is a provably correct refinement of the original problem specification.
Specware allows you to express requirements as formal specifications without regard to the ultimate implementation or target language. Specifications can describe the desired functionality of a program independently of such implementation concerns as architecture, algorithms, data structures, and efficiency. This makes it possible to focus on the correctness, which is crucial to the reliability of large software systems.
Often, there are many possible solutions to a single problem, all valid, with different advantages and drawbacks. It is sometimes very difficult to make a decision given all the different trade-offs. Using Specware, the analysis of the problem can be kept separate from the implementation process, and implementation choices can be introduced piecemeal, making it easier to backtrack or explore alternatives.
Specware allows you to articulate software requirements, make implementation choices, and generate provably correct code in a formally verifiable manner. The progression of specifications forms a record of the system design and development that is invaluable for system maintenance. You can later adapt the specifications to new or changed requirements or make different implementation decisions at any level of the development while reusing what has not changed, and generate provably correct new code by the same process.