Report Number: CSL-TR-87-335
Institution: Stanford University, Computer Systems Laboratory
Title: Allocations of Objects Considered as Nondeterministic
Expressions - Towards a More Abstract Axiomatics of Access
Types
Author: Meldal, Sigurd
Date: September 1987
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.
http://i.stanford.edu/pub/cstr/reports/csl/tr/87/335/CSL-TR-87-335.pdf