BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CS-TR-76-549
       ENTRY:: July 04, 1995
ORGANIZATION:: Stanford University, Department of Computer Science
       TITLE:: Automatic program verification V: verification-oriented proof
               rules for arrays, records and pointers
        TYPE:: Technical Report
      AUTHOR:: Luckham, David C.
      AUTHOR:: Suzuki, Norihisa
        DATE:: March 1976
       PAGES:: 52
    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.
       NOTES:: [Adminitrivia V1/Prg/19950704]
         END:: STAN//CS-TR-76-549