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

transformations are used, meaning we can directly use the lemmas associated
with these transformations. Such an automatic association is, as we say in the
conclusion, a future work.

7Con lu on

The approach presented in this paper allows a user of the rCOS tool to auto-
matically generate proof obligations of design refinement. The generated state-
ments are defined using the predicate transformer semantics mechanized in [24]
extended here to support object-oriented programs, thanks to a graph-based
representation of the memory. A library of lemmas and theorems is available
to the user in order to help her to prove the generated statements, concerning
for instance the graph operations or the refinement calculus. There are two ma-
jor strengths to this approach. The first one is the seamless integration within
the rCOS tool, hence making the process transparent for the user, who can
design a software using UML, with the proof obligations being automatically
generated. Of course, these obligations still have to be discharged, but using a
more generic back-end, like Why [9], would generate proof statements both for
interactive theorem provers and automated demonstrators. However, since we
are using higher-order terms, automated demonstration might not be very e-
cient, therefore we need to keep providing lemmas corresponding to refinement
steps, especially the ones concerning concepts. This issue poses the one of

the scalability, since large programs usually involve a large number of refinement
rules and a statement containing a large number of rules can only be proven in
a reasonable amount of time and space if each rule has been proven for the
general case. The proof would then only be a succession of application of simple
rules, which is the main strength of the refinement calculus. We therefore believe
that the effort should be made to provide the developer with a large number
of rules already proven rather than trying to automatically prove a complex
transformation.
The other strength of this approach is the definition of the graph-based seman-
tics. Although using a graph is not strictly more expressive than using records
or a function from pointers to values, that is, it does not allow one to express
more programs, the properties of a state can be expressed in a different, more
abstract and intuitive way. In particular, the graph model helps the formulation
and understanding of properties in the first place and on the other hand provides
intuition for construction of their proofs to be checked by the theorem prover. In
practice, the function getEdgeFun of a graph is conceptually close to a function
from pointers to values: each object node is a pointer and each value node is a
value. In other words, a graph can be seen as an extensional definition of a usual
function from pointers to value. However we believe that a more abstract view of
the memory helps reasoning about the state of the program. For instance, stat-
ing that a path p is alias-free in a state g is simply done by stating that there is
no path p2 different from p such that getVertexPath p g = getVertexPath p2 g .
Several limitations need however to be addressed, for instance the assumption
isGoodPath in the theorem swingPathChangeVertex or in the weakest precondition

oo