Reasoning about Assignments in Recursive Data Structures - Formal Methods: Foundations and Applications - page 163

coproduct type can be constructed with lab i ( M ) ,where M : ρ i , and recognised

with lab i ? . Standard set comprehension notation can be used to define predicate

subtypes. New types can be introduced via definitions, like

{ bottom , up ( down : σ )}
( bottom is the unit type and we omit its argument). The lift type constructor
adds a bottom element to an arbitrary type σ given as a parameter, written in
short as σ ⊥ =

lift [ σ ] : TYPE =

[ σ ]

lift .

Lists are defined as
list [ σ ] : TYPE = { null , cons ( car : σ , cdr : list )}

++

There is an infix function that appends two lists. It is overloaded so that

when one of its arguments is of type σ , then this argument is converted to a list.
The i th element of a list l can be accessed using nth ( l , i ) .

3 The Model

This section describes an operational semantics of a core object-oriented lan-
guage. The focus is on the features needed to understand the properties discussed
in the next section, i.e., we do not model some typical object-oriented features
like inheritance. The interested reader can find the full PVS formalisation at
http://cs.ru.nl/~tamalet .

3.1 The Heap

In our model we consider all values to be an object or void. The set Object is
defined as an uninterpreted type that represents non-void objects. Instances of
Object v have the possibility of being void :
Object v : TYPE =

{ obj ( obj : Object ), void }
A basic approach to model the heap, due to Burstall [5] and more recently
emphasised by Bornat [3], is to model it as a collection of functions of type
Object → Object v , one for each class field (i.e. the component). This mod-
elling encodes the fact that changing to what object a field points to does not
affect other fields. This has the important consequence that whenever one field
is updated, we do not need to propagate that update to the other fields. This is
sometimes called the component-as-array model [7,9].
Our heap is a grouping of field functions, indexed by their field names:

[ Object → Object v ]]
where Name is a set representing the field names. Given a heap h and a field
name f , h ( f )

Heap : TYPE =

[ Name →

is the corresponding field function. This indexing allows us to reason
about field names, which is not possible when using a loose set of field functions as
in the component-as-array model. There, the names of the fields are fixed by the
names of the functions that model them. We use this to express meta-properties