Automatic program verification V: verification-oriented proof rules for arrays, records and pointers
Abstract/Contents
- Abstract
- A practical method is presented for automating in a uniform way the verification of Pascal programs that operate on the standard Pascal data structures ARRAY, RECORD, and POINTER. New assertion language primitives are introduced for describing computational effects of operations on these data structures. Axioms defining the semantics of the new primitives are given. Proof rules for standard Pascal operations on pointer variables are then defined in terms of the extended assertion language. Similar rules for records and arrays are special cases. An extensible axiomatic rule for the Pascal memory allocation operation, NEW, is also given. These rules have been implemented in the Stanford Pascal program verifier. Examples illustrating the verification of programs which operate on list structures implemented with pointers and records are discussed. These include programs with side-effects.
Description
| Type of resource | text |
|---|---|
| Form | technical reports |
| Extent | 1 text file |
| Place | Stanford (Calif.) |
| Date created | March 1, 1976 |
| Language | English |
| Digital origin | reformatted digital |
Creators/Contributors
| Author | Luckham, David C. | |
|---|---|---|
| Author | Suzuki, Norihisa |
Subjects
| Subject | Stanford University. Computer Science Department |
|---|---|
| Subject | Computer science |
| Genre | Technical reports |
Bibliographic information
| Finding Aid | |
|---|---|
| Technical Report # | CS-TR-1976-549 |
| Location | https://purl.stanford.edu/kb470yn0165 |
| Location | 3840/2 |
| Repository | Stanford University. Libraries. Department of Special Collections and University Archives |
Access conditions
- Use and reproduction
- The materials are open for research use and may be used freely for non-commercial purposes with an attribution. For commercial permission requests, please contact the Stanford University Archives (universityarchives@stanford.edu).
Collection
Stanford Artificial Intelligence Laboratory records, 1963-2009
View other items in this collection in SearchWorksStanford University, Department of Computer Science, Technical Reports
View other items in this collection in SearchWorksAlso listed in
Loading usage metrics...