Automatic Program Verification V: Verification-Oriented Proof Rules for Arrays, Records, and Pointers

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.

Open PDF

Document Details

Document Type
Technical Report
Publication Date
Mar 01, 1976
Accession Number
ADA027455

Entities

People

  • David Luckham
  • Norihisa Suzuki

Organizations

  • Stanford University

Tags

Communities of Interest

  • Autonomy

DTIC Thesaurus Topics

  • Artificial Intelligence
  • Atomic Properties
  • Automatic
  • Computations
  • Computer Languages
  • Computer Science
  • Computers
  • Language
  • Notation
  • Programming Languages
  • Sequences
  • Short Circuits
  • Side Effects
  • Standards
  • Universities
  • Verification

Readers

  • Artificial Intelligence
  • Computer Science.
  • Database Systems and Applications