BIB-VERSION:: CS-TR-v2.0
          ID:: STAN//CSL-TR-87-335
       ENTRY:: November 08, 1994
ORGANIZATION:: Stanford University, Computer Systems Laboratory
       TITLE:: Allocations of Objects Considered as Nondeterministic
               Expressions - Towards a More Abstract Axiomatics of Access
               Types
        TYPE:: Technical Report
      AUTHOR:: Meldal, Sigurd
        DATE:: September 1987
       PAGES:: 21
    ABSTRACT:: The concept of access ("reference" or "pointer") values is
               formalized as parametrized abstract data types, using the
               axiomatic method of Guttag and Horning as extended by Owe.

               Two formalizations are given. The first is a formalization of
               the approach used in the definition of a partial correctness
               system for Pascal by Hoare and Wirth. Its lack of abstraction
               is pointed out. This is caused by the annotation language
               being too expressive. An approach is taken which results in a
               more abstract system: The expressiveness of the annotation
               language is reduced and the allocation operator is viewed as
               a nondeterministic expression. This reinterpretation of the
               program language results in an appropriate level of
               abstraction of the proof system.

               An example is given, verification of a package defining a set
               type.
       NOTES:: [Adminitrivia V1/Prg/19941108]
         END:: STAN//CSL-TR-87-335