Mechanical Proofs about Computer Programs
Abstract
The Gypsy verification environment is a large computer program that supports the development of software systems and formal, mathematical proofs about their behavior. The environment provides conventional development tools, such as a parser for the Gypsy language, an editor and a compiler. These are used to evolve a library of components that define both the software and precise specifications about its desired behavior. The environment also has a verification condition generator that automatically transforms a software component and its specifications into logical formulas which are sufficient to prove that the component always runs according to specification. Facilities for constructing formal, mechanical proofs of these formulas also are provided. Many of these proofs are completed automatically without human intervention. The capabilities of the Gypsy system and the results of its applications are discussed.
Document Details
- Document Type
- Technical Report
- Publication Date
- Mar 01, 1984
- Accession Number
- ADA494739
Entities
People
- Donald I. Good
Organizations
- University of Texas at Austin