The Application of Formal Specifications to Software Documentation and Debugging.
Abstract
This paper illustrates the application of formal specifications to software documentation and debugging by presenting a real-life scenario involving the use of a garbage collection package. It illustrates the advantages of using formal specifications over informal documentation. The paper also illustrates the usefulness of run-time checking tools that compares program behavior with their formal specifications. The scenario presented in this paper goes through a series of steps that include formal specification, run-time checking, and modification of the specification and program based on the results of run-time checking - the typical steps involved in a debugging process, except that this scenario makes use of formal specifications. Although various research ideas presented in this paper have been published earlier, this paper assimilates all these ideas into a real-life scenario, and illustrates in an easy-to-understand way that these ideas are really useful to software documentation and debugging. The example has been developed in Ada, and formally specified using the Anna specification language. The tool used in the example is the Anna Run-Time Consistency Checking System developed at Stanford University.
Document Details
- Document Type
- Technical Report
- Publication Date
- Apr 01, 1993
- Accession Number
- ADA311463
Entities
People
- Anoop Goyal
- Sriram Sankar
Organizations
- Stanford University