BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CSL-TR-90-436
       ENTRY:: November 08, 1994
ORGANIZATION:: Stanford University, Computer Systems Laboratory
       TITLE:: APPLICATION OF FORMAL SPECIFICATION TO SOFTWARE MAINTENANCE
        TYPE:: Technical Report
      AUTHOR:: Madhav, Neel
      AUTHOR:: Sankar, Sriram
        DATE:: August 1990
       PAGES:: 15
    ABSTRACT:: This paper describes the use of formal specifications and
               associated tools in addressing various aspects of software
               maintenance ---corrective, perfective, and adaptive. It also
               addresses the refinement of the software development process
               to build programs that are easily maintainable. The task of
               software maintenance in our case includes the task of
               maintaining the specification as well as maintaining the
               program.

               We focus on the use of Anna, a specification language for
               formally specifying Ada programs, to aid us in maintaining
               Ada programs. These techniques are applicable to most other
               specification language and programming language environments.
               The tools of interest are: (1) the Anna Specification
               Analyzer which allows us to analyze the specification for
               correctness with respect to our informal understanding of
               program behavior; and (2) the Anna Consistency Checking
               System which monitors the Ada program at runtime based on the
               Anna specification.
       NOTES:: [Adminitrivia V1/Prg/19941108]
         END:: STAN//CSL-TR-90-436