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

about multidot field expressions in Section 4. The separation by syntax provided
by the component-as-array model is lost in this model, because a field update is
now an update on the heap function. With the meta-level properties presented
in the rest of this paper, we obtain a reincarnation of separation by syntax.
The above definition of the heap highlights the relationship with the compo-
nent-as-array model. However, defining the heap as a function of type

[

Object

→ [ may seem more intuitive. In this definition we first fix an

object and then we ask for a field name to obtain its value. As the functions
are total (required by PVS), both definitions are in fact equivalent. This means
that every field should be defined at every object. This is of course not realistic,
however, accesses to undefined fields can be handled by a preliminary static
analysis.

→

Object v ]] Name

3.2 Expressions, Statements and Compositions

We model expressions, statements and their compositions following Meyer's ideas
for a semantics for Eiffel [12]. A distinctive aspect of this approach is that ex-
pressions and statements are evaluated relative to an object, which is provided
together with the heap as argument.
We deal with null-pointer dereferencing in language constructs, as opposed to
avoiding it by type constraints. In our experience, the second approach leads to
cumbersome specifications because the result of each expression and statement
must be checked for definedness before composing them.
There are two syntactic categories: expressions (without side-effects) and
statements:

Expr : TYPE =

{ e: [ Object v ⊥ , Heap ⊥ → Object v ⊥ ] |

∀ ( o:Object v ⊥ , h:Heap ⊥ ) :

bottom_or_void? ( o , h )

⇒

bottom? ( e ( o , h ))}

Stmt : TYPE =

{ S: [ Object v ⊥ , Heap ⊥ →

Heap ⊥ ] |

∀ ( o:Object v ⊥ , h:Heap ⊥ ) :

bottom_or_void? ( o , h )

⇒

bottom? ( S ( o , h ))}

To define a semantics for Eiffel, Meyer works with partial functions [12]. In most
theorem provers, including PVS, functions have to be total. For this reason we
use lifted arguments, to represent undefinedness. The bottom _ or _ void )

predicate returns true if and only if o is undefined or void or h is undefined. By
using predicate subtypes, we ensure that whenever an expression or statement
is evaluated in void or in an undefined object or state, the result is undefined.
This shifts checking for void or bottom from the specification to type correctness
obligations that PVS generates automatically.
The expression Current (called this or self in some languages) returns the
current object:

?(

o , h

Current : Expr =

λ ( o:Object v ⊥ , h:Heap ⊥ ) :
IF bottom_or_void? ( o , h ) THEN bottom ELSE o