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

of the statements, which may be too strong. Intuitively, this theorem still holds
without it but the proof is more complex, since in general we lose the fact that
the owner of the path is the same before and after swinging, as we showed on
the examples. A possible lead to address this issue is to consider that any path
which does not satisfy isGoodPath can be “reduced” to a path which does. For
instance, on Figure 1 (b), the path v.a.b.c.a points to the same object that v.a
points to, but v.a satisfies isGoodPath .
Moreover, more designs need to be implemented in the translation process, for
instance recursive method calls. However, we can extensively reuse [8,14], defined
for imperative programs, by extending them to object-oriented programs. The
method call does not currently support dynamic binding, but it could be done
by looking up the actual type of the caller from the second element onodefun of
the graph to fix the called method body.
In general, the next step is to integrate this mechanism within model trans-
formations, which is an on-going work in the rCOS tool [21]. The principal
challenge in this work is for the tool to handled¡ several models at the same
time: before, during and after refinement. Such modifications are easy to han-
dle when changing the design of a single method, but more complicated when
for instance changing or deleting classes. The idea is then to establish a corre-
spondence between the modifications done in the tool and the refinement rules
involved. Moreover, a better interaction with Isabelle could help the user in the
decomposition of the refinement steps. For instance, by using similar techniques
than those used in automated demonstration, the tool could use the feedback
from the theorem prover to ask the user to introduce more steps. We then could
have a system where the user introduces a refinement rule, the tool tries to
prove it automatically, if it cannot, it asks the user for an intermediary step,
tries again, and so on until the whole rule is proved.
Acknowledgment. This work has been supported by the project GAVES of
the Macao S&TD Fund, the 973 program 2009CB320702, STCSM 08510700300,
and the projects NSFC-60721061, NSFC-60970031, NSFC-90718041 and NSFC-
60736017. The authors would like to thank Volker Stolz for his useful remarks.
References
1. Back, R.-J.: On the Correctness of Refinement Steps in Program Development.
PhD thesis, Helsinki, Finland, Report A-1978-4 (1978)
2. Back, R.-J., Fan, X., Preoteasa, V.: Reasoning about pointers in refinement cal-
culus. Technical Report 543, TUCS - Turku Centre for Computer Science, Turku,
Finland (July 2003)
3. Carrington, D., Hayes, I., Nickson, R., Watson, G., Welsh, J.: A tool for developing
correct programs by refinement. In: Proc. BCS 7th Refinement Workshop. Springer,
Heidelberg (1996)
4. Cavalcanti, A., Naumann, D.A.: A weakest precondition semantics for refinement of
object-oriented programs. IEEE Transactions on Software Engineering 26, 713-728
(2000)