Verification of APL Programs.
Abstract
APL is of interest with regard to program verification for two reasons; many loops may be expressed in the structured operators, resulting in fewer assertions and thus easier verification for some programs, especially those with arrays, and the partial operators introduce the complication of showing that a program is executable. A formal definition of the APL operators serves as the base for a deductive system in which it is possible to informally prove assertions about APL programs. A mechanical system is described which generates preconditions for proper program executability. Several programs are verified. (Author)
Document Details
- Document Type
- Technical Report
- Publication Date
- Nov 01, 1972
- Accession Number
- AD0754856
Entities
People
- Susan Lucille Gerhart
Organizations
- Carnegie Mellon University