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

The operators compose expressions and statements. If x is an expression,

S an statement and r is either of them, we define:
S ; r =

and ;

￿

λ ( o:Object v ⊥ , h:Heap ⊥ ) :r ( o , S ( o , h ))

λ ( o:Object v ⊥ , h:Heap ⊥ ) :r ( x ( o , h ), h )
The normal uses are state compositions S ; T and field access x ￿ y . The overloading
allows us also to write S ; x , which returns the value of evaluating x after the
statement S ,and x ￿ S , which can be thought as a qualified call of S from x .
We define in PVS an automatic conversion that translates a name f into
the expression λ ( o: Object v ⊥ , h: Heap ⊥ ) :h ( f )( o ) whenever needed. This
allows us to express a field access directly as x ￿ f . We also define a conversion
that translates an o : Object into obj ( o ): Object v , and one that translates an
o : Object v into up ( o ): Object v ⊥ , to reduce the amount of syntax.
IF -statements are mapped to IF -expressions in the logic of PVS. For reasons
of succinctness we omit the treatment of WHILE .

x ￿ r =

3.3 Assignments

At its core, an assignment is an update of a heap-function in a particular point
(consisting of a field and an object):

update ( f : Name , p : Object , h : Heap , q : Object_v ) : State

=

λ ( g : Name )( o : Object ) :
IF p = o ∧ f = g THEN q ELSE h ( g )( o )

Our model forces us to explicitly deal with undefinedness due to dereferencing
of void. The update operation is encapsulated in an operator

:=

that assigns an

object q to the field f of the object p in the heap h : 1

= ( f : Name , q:Object v ) : Stmt =

:

λ ( p:Object v ⊥ , h:Heap ⊥ ) :
IF bottom_or_void? ( p )

bottom? ( h ) THEN bottom
ELSE update ( f , obj ( down ( p )), down ( h ), q )

∨

If the assignment is made in an undefined state or tries to assign to void, the
error is propagated. This is required by the definition of Stmt . We shall use the
above variable names throughout the rest of this paper. The next step is to define
local assignments f

e 2 . These definitions
are not relevant for the development of this paper and we therefore omit them.
An assignment affects a field access if and only if the object where the field is
evaluated is the one where the assignment was made and the field being accessed
is the one that was assigned to. This is summarised in the following two basic
separation and interference properties (both assume that o , h is not bottom or
void):

:=

e and qualified assignments e 1 ￿ f

:=

Property 1. If p = o or f = g ,then g ( o , ( f := q )( p , h )) = g ( o , h ) .

1 In the PVS formalisation we have called this function < = ,because := is reserved.