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

The refinement for Component and Object Systems (rCOS) [10,16] method
provides an interesting framework to address these challenges. Firstly, rCOS
has a formal semantics based on an extension of the Unifying Theories of Pro-
gramming (UTP) [11] to include the concepts of components and objects. The
graph-based operational semantics [12] has recently been defined for

pro-
grams. Secondly, the rCOS tool (available at http://rcos.iist.unu.edu )provides
a UML-like multi-view and multi-notational modeling and design platform. In
particular, two verification processes are already implemented: the automated
generation of test cases to check the robustness of a component [15], and the
automated generation of CSP processes to verify the compatibility between the
sequence diagram and the state diagram of a contract [7]. Lastly, rCOS extends
the refinement calculus [1,17], which is a program construction method, where
a non-deterministic specification is incrementally refined to deterministic code,
using pre-defined rules. This approach creates several refinement steps, which
fill the gap between the specification and the implementation, therefore reduces
the proof complexity, by replacing a single complex proof by many simpler ones.

oo

Related Work. The mechanization of the refinement calculus was firstly done
in [24], which has been extended to include pointers [2] and also object-oriented
programs [4,20]. In particular, a refinement calculus has been defined for Eiffel
contracts [19], and encoded in PVS [18]. Although this approach addresses a
similar issue than the one exposed here, the authors encode the calculus using a
shallow embedding, that is, a class in Eiffel is encoded as a type in PVS, a routine
in Eiffel is encoded as a function in PVS, etc. Proofs of refinement are then done
over PVS programs rather than PVS terms , and so require the understanding of
the underlying semantics of PVS. We use here a deep embedding, following [24],
and the proofs of refinement are done, roughly speaking, over the abstract syntax
tree of the original program, and so only require to know how to write a proof
in Isabelle/Isar. The Program Refinement Tool [3] provides a deep embedding
of a refinement calculus, and even if it does not support

programs natively,
it could be extended with an existing formalization which does [22]. However,
rCOS also provides a semantics for components, and even if we do not address in
this paper the issue of verification of component protocols, this work is part of a
larger framework where other verification techniques exist [21]. In other words,
the work presented here is not a standalone tool, but adds up to a collection of
tools that helps a developer to specify, implement and verify an application.
On the other hand, different memory models for object-oriented programs
have been encoded in theorem provers [9,23,13]. However, the memory in these
approaches is either modelled as a function from addresses or pointers to values or
using records to represent objects. Although such a modelling is very expressive,
and has been shown to be adapted to automated demonstration, we propose here
a representation of the memory by a directed and labeled graph, that is intuitive
than a representation by a function or set of records. The graph structure helps
in the formulation of properties and carrying out interactive proofs.

OO