Software evolution, enhancement, and maintenance is the most time-consuming and error-fraught phase of the conventional software-production process, because even apparently small changes at the code level can have unanticipated and disastrous consequences. This occurs when a single design element may have ramifications in many places in the code, all of which must be changed in a coordinated way. It is common for a critical piece of software to be frozen long after it is obsolete, because no one dares to update it. Why should things be any better in a system produced with Specware?
A Specware refinement constitutes a complete record of the design history of a system, from specification to code. When changes are made to the requirements or the environment, alterations are made to the specification, not to the code directly. The refinement process is repeated on the altered specification; as much as possible of the previous refinement is retained. If part of the earlier refinement no longer applies, it must be altered accordingly. A small change at the specification level may be implemented by many diffuse changes at the code level, but at no point are changes in the specification allowed to compromise the correctness of the final product. Consequently we may be more adventurous and experimental in altering a system implemented via Specware. It may turn out that the greatest benefits from the use of Specware will accrue not from the initial implementation but from the ease and reliability of subsequent modification and enhancement of the software.