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

Object Creation. The command object implements object creation s. new ( p ):
definition object :: path ⇒ ctype ⇒ (graph pred) ⇒ (graph pred) where
object p s q ≡ λ u. wfGraph u & wfPath p u & wflabelExpF (getAttrsOfCtype s) u
& q (addObject p s u)
5.2 Composite Designs
With the predicate transformer semantics, the definitions of the composite de-
signs, like the sequential composition, the loop or the conditional statement,
do not depend on the representation of the memory state. Hence, we can di-
rectly re-use the definitions and theorems from [24]. For instance, the sequential
composition c; d is refined by e; f if c is refined by e and d is refined by f
and c is monotonic, and in fact, we have proved that all basic commands (i.e.
nondass , pp , assign , begin and end ) are monotonic, and the compound constructs
locdec, method, cond, do, seq preserve monotonicity with respect to their sub-
components. Moreover, the other constructs such as the conditional cond and the
loop do preserve refinement with respect to their subcomponents. By applying
these theorems, we can refine a program by repeatedly refining its subcompo-
nents, and then prove that the new generated program is a refinement of the old
one.
6 Application
We describe in this section how to use the mechanization of the refinement
calculus within the rCOS tool.
6.1 Tool Refinement
Refining a model is, by definition, a dynamic process: a new model is generated
from a previous one, by applying some refinement rules. The main challenge is
then to be able to consider both models at the same time, in order to generate
the corresponding proof obligations. When the refinement concerns only method
bodies, the rCOS tool provides a simple way to define a refinement operation.
Firstly, a class is created, and stereotyped with a specific kind of refinement, for
instance refining automatically every [ true |− x'=e] by x:=e . The most general
refinement is the manual refinement, where the user provides an operation, its
old design (mainly for sanity checks), and the refining design. In a second step,
the user can, at any time, apply such a refinement by right-clicking on the
corresponding class and selecting the “refine” operation, and the tool will then
transform the model accordingly.
6.2 Provided Lemmas
In addition to the theorems introduced in [24], we provide lemmas corresponding
to refinement steps. For instance, the lemma stating that for any path p and any
integer expression n , [ true |− p'=n] is refined by p:=n is defined as: