Application of formal specification to software maintenance

The authors describe the use of formal specifications and associated tools in addressing various aspects of software maintenance-corrective, perfective, and adaptive. They also address the refinement of the software development process to build programs that are easily maintainable. The task of software maintenance in this case includes the task of maintaining the specification, as well as the program. The authors focus on the use of Anna, a specification language for formally specifying Ada programs, to aid in maintaining Ada programs. The techniques are applicable to most other specification language and programming language environments. The tools of interest are (1) the Anna Specification Analyzer, which permits analysis of the specification for correctness with respect to the informal understanding of program behavior; and (2) the Anna Consistency Checking System, which monitors the Ada program at run time on the basis of the Anna specification