Access Restriction

Author Levitt, Karl N. ♦ Robinson, Lawrence
Source ACM Digital Library
Content type Text
Publisher Association for Computing Machinery (ACM)
File Format PDF
Language English
Subject Keyword And programming methodology ♦ Structured programming ♦ Formal specification ♦ Abstraction ♦ Program verification ♦ Hierarchical structure
Abstract A method for describing and structuring programs that simplifies proofs of their correctness is presented. The method formally represents a program in terms of levels of abstraction, each level of which can be described by a self-contained nonprocedural specification. The proofs, like the programs, are structured by levels. Although only manual proofs are described in the paper, the method is also applicable to semi-automatic and automatic proofs. Preliminary results are encouraging, indicating that the method can be applied to large programs, such as operating systems.
Description Affiliation: Stanford Research Institute, Menlo Park, CA (Robinson, Lawrence; Levitt, Karl N.)
Age Range 18 to 22 years ♦ above 22 year
Educational Use Research
Education Level UG and PG
Learning Resource Type Article
Publisher Date 2005-08-01
Publisher Place New York
Journal Communications of the ACM (CACM)
Volume Number 20
Issue Number 4
Page Count 13
Starting Page 271
Ending Page 283

Open content in new tab

   Open content in new tab
Source: ACM Digital Library