Accession Number : ADA311463

Title :   The Application of Formal Specifications to Software Documentation and Debugging.

Descriptive Note : Technical note,

Corporate Author : STANFORD UNIV CA COMPUTER SYSTEMS LAB

Personal Author(s) : Goyal, Anoop ; Sankar, Sriram

PDF Url : ADA311463

Report Date : APR 1993

Pagination or Media Count : 21

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.

Descriptors :   *SOFTWARE ENGINEERING, *DEBUGGING(COMPUTERS), COMPUTER PROGRAM DOCUMENTATION, ALGORITHMS, SCENARIOS, COMPUTER COMMUNICATIONS, SPECIFICATIONS, INPUT OUTPUT PROCESSING, SYSTEMS ANALYSIS, SUBROUTINES, COMPUTER PROGRAM VERIFICATION, ADA PROGRAMMING LANGUAGE, EXECUTIVE ROUTINES, AUTOMATIC PROGRAMMING.

Subject Categories : Computer Programming and Software

Distribution Statement : APPROVED FOR PUBLIC RELEASE