A Graph-Based Implementation for Mechanized Refinement Calculus of OO Programs - Formal Methods: Foundations and Applications - page 267

We are now in position to introduce the function addObject which creates a
new vertex (object) in a graph. Given a path l ,aclasstype s and a graph g ,this
function first gets a fresh object node of type s not in g ,doneby getNodeFromType ;
then swings the path l to refer to the new vertex by using swingPath ; and fi-
nally, attaches the attributes of class s to the new node and initialises them,
which is implemented by the function addAttrs . In the definition, the function
getAttrsOfCtype is used to extract the attribute information from class s .

definition addObject:: path ⇒ ctype ⇒ graph ⇒ graph where
addObject l s g ≡ let v = (N (getNodeFromType s g)) in addAttrs v
(expToNode (getAttrsOfCtype s) g) (swingPath l v g)

The functions removeSnode , Vars and addObject are proved to preserve the graph
well-formedness, and furthermore, the last two are proved to ensure that vari-
ables or attributes are initialised with the correct values.

5 Refinement of rCOS Designs

The graph-based representation of the memory presented in the previous section
allows us to extend the mechanization of the refinement calculus presented in
Section 3 to deal with object-orientation. Since we only consider well-formed
graphs and paths, we integrate these conditions into the weakest precondition
of each command. The complete definition of the refinement calculus for all
constructs can be found at http://isg.rhul.ac.uk/morisset/sbmf/rcos.thy .

5.1 Primitive Designs

Pre/post-condition. The definition of the non-deterministic assignment is
changed to include the well-formedness checks.

definition
nondass :: (graph (graph pred) where

nondass P l q ≡ ( λ v. (wfGraph v) & (wfPathl l v) & ( ∀ v1. P v v1 ⇒ qv1))

⇒ graph pred) ⇒ path list ⇒ (graph pred) ⇒

where wfPathl l v is true if, and only if, every path in l satisfies wfPath . This list
of paths corresponds to all the paths appearing in the post-condition. A pre/post-
condition is then an assertion followed by a non-deterministic assignment.

definition pp :: (graph pred) ⇒ (graph ⇒ graph pred) ⇒ path list ⇒
(graph predT) where
pppr l ≡ assert p ; nondass r l

where assert is the standard definition for the assertion. For instance, the
pre/post-condition [ true |− a.b.x'=2] is translated into the following statement

pp (true) ( λ g. λ g1.((getIntOfPath a.b.x g1) = 2)) [ a.b.x ]