Automating Refinement of Circus Programs - Formal Methods: Foundations and Applications - page 289

the UTP. On the other hand, it does not specify a model for its deductive sys-
tem and calculus, and this imposes limitations on proving consistency of theory
extensions. An interesting line of work could be to try and combine Saoithın
with our tools to see if we can reap individual benefits of both of them.
Future work will first consist of mechanising the entire refinement strategy
for control laws in [13]. Secondly, further work is required to provide proof au-
tomation in relation to the well-definedness of the initial program. To obtain
unqualified theorems, those assumptions need to be discharged. It is still an
open issue how provisos in such theorems are best proved, and whether some of
the wd theorems that we discard as we go along should be cached for later use.
Acknowledgements. This work has been funded by EPSRC as part of the Pro-
gramming from Control Laws research grant EP/E025366/1.
References
1. Butterfield, A.: Saoithın Proof Assistant,
http://www.scss.tcd.ie/Andrew.Butterfield/Saoithin/
2. Cavalcanti, A., Clayton, P., O'Halloran, C.: Control Law Diagrams in Circus .In:
FM 2005: Formal Methods. LNCS, vol. 3582, pp. 253-268. Springer, Heidelberg
(2005)
3. Cavalcanti, A., Clayton, P., O'Halloran, C.: From Control Law Diagrams to Ada
via Circus . Technical report, University of York, York, U.K. (April 2008)
4. Cavalcanti, A., Sampaio, A., Woodcock, J.: A Refinement Strategy for Circus .For-
mal Aspects of Computing 15(2-3), 146-181 (2003)
5. Dijkstra, E.: A Discipline of Programming. Prentice Hall Series in Automatic Com-
putation. Prentice Hall, Englewood Cliffs (1976)
6. Hoare, C.A.R., Jifeng, H.: Unifying Theories of Programming. Prentice Hall Series
in Computer Science. Prentice Hall, Englewood Cliffs (1998)
7. Martin, A., Gardiner, P., Woodcock, J.: A Tactic Calculus - Abridged Version.
Formal Aspects of Computing 8(4), 479-489 (1996)
8. Morgan, C.: Programming from Specifications. Prentice Hall International Series
in Computer Science. Prentice Hall, Englewood Cliffs (1998)
9. Oliveira, M.: Formal Derivation of State-Rich Reactive Programs using Circus .PhD
thesis, Department of Computer Science, University of York (2005)
10. Oliveira, M., Cavalcanti, A.: ArcAngelC : a refinement tactic language for Circus .
Electronic Notes in Theoretical Computer Science 214, 203-229 (2008)
11. Oliveira, M., Cavalcanti, A., Woodcock, J.: ArcAngel : a Tactic Language for Re-
finement. Formal Aspects of Computing 15(1), 28-47 (2003)
12. Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal
Aspects of Computing, Online First (December 2007)
13. Oliveira, M., Cavalcanti, A., Zeyda, F.: A Tactic Language for Refinement of State-
Rich Concurrent Specifications (to appear)
14. Oliveira, M., Xavier, M., Cavalcanti, A.: Refine and Gabriel: Support for Refine-
ment and Tactics. In: Proceedings of the Second Int. Conference on Software Engi-
neering and Formal Methods, pp. 310-319. IEEE Computer Society, Los Alamitos
(2004)