UTPCalc — A Calculator for UTP Predicates

  • Andrew ButterfieldEmail author
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 10134)


We present the development of the UTP-Calculator: a tool, written in Haskell, that supports rapid prototyping of new theories in the Unifying Theories of Programming paradigm, by supporting an easy way to very quickly perform test calculations. The emphasis during the calculator development was keeping it simple but effective, and relying on the user to have the expertise to check its output. It is not intended to supplant existing theorem prover or language transformation technology. The tool is designed for someone who is both very familiar with UTP theory construction, and familiar enough with Haskell to be able to write pattern-matching code. In this paper we describe how this tool can be used to assist in theory development, by describing the key components of the calculator and how various aspects of such a theory might be encoded. We finish with a discussion of our experience in using the tool.


Theorem Prover Dictionary Entry Sequential Composition Expression Equality Loop Unroll 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. 1.
    Bauer, F.L., Ehler, H., Horsch, A., Möller, B., Partsch, H., Paukner, O., Pepper, P.: The Munich Project CIP, Volume II: The Program Transformation System CIP-S. LNCS, vol. 292. Springer, Heidelberg (1987). doi: 10.1007/3-540-18779-0 CrossRefGoogle Scholar
  2. 2.
    Bertot, Y., Castéran, P.P.: Interactive Theorem Proving and Program Development: Coq’Art: The Calculus of Inductive Constructions. Texts in Theoretical Computer Science. Springer, Heidelberg (2004)CrossRefzbMATHGoogle Scholar
  3. 3.
    Bird, R.: Thinking Functionally with Haskell. Cambridge University Press, Cambridge (2014)CrossRefGoogle Scholar
  4. 4.
    Butterfield, A.: Saoithín: a theorem prover for UTP. In: Proceedings of Unifying Theories of Programming - Third International Symposium, UTP 2010, Shanghai, China, 15–16 November 2010, pp. 137–156 (2010).
  5. 5.
    Butterfield, A.: The logic of \(U \cdot (TP)^{2}\). In: Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, 27–28 August 2012, Revised Selected Papers, pp. 124–143 (2012).
  6. 6.
    Butterfield, A., Mjeda, A., Noll, J.: UTP semantics for shared-state, concurrent, context-sensitive process models. In: Bonsangue, M., Deng, Y. (eds.) TASE 2016 10th International Symposium on Theoretical Aspects of Software Engineering, pp. 93–100, IEEE, July 2016Google Scholar
  7. 7.
    Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: The Maude 2.0 system. In: Nieuwenhuis, R. (ed.) RTA 2003. LNCS, vol. 2706, pp. 76–87. Springer, Heidelberg (2003). doi: 10.1007/3-540-44881-0_7 CrossRefGoogle Scholar
  8. 8.
    Foster, S., Woodcock, J.: Mechanised theory engineering in isabelle. In: Irlbeck, M., Peled, D.A., Pretschner, A. (eds.) Dependable Software Systems Engineering, NATO Science for Peace and Security Series, D: Information and Communication Security, vol. 40, pp. 246–287. IOS Press (2015).
  9. 9.
    Foster, S., Zeyda, F., Woodcock, J.: Isabelle/UTP: a mechanised theory engineering framework. In: Naumann, D. (ed.) UTP 2014. LNCS, vol. 8963, pp. 21–41. Springer, Heidelberg (2015). doi: 10.1007/978-3-319-14806-9_2 Google Scholar
  10. 10.
    Hughes, J.: The design of a pretty-printing library. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 53–96. Springer, Heidelberg (1995). doi: 10.1007/3-540-59451-5_3. CrossRefGoogle Scholar
  11. 11.
    Marlow, S. (ed.): Haskell 2010 Language Report. Haskell Community (2010).
  12. 12.
    Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). zbMATHGoogle Scholar
  13. 13.
    Nuka, G., Woodcock, J.: Mechanising a unifying theory. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 217–235. Springer, Heidelberg (2006). doi: 10.1007/11768173_13 CrossRefGoogle Scholar
  14. 14.
    Shankar, N.: PVS: combining specification, proof checking, and model checking. In: Srivas, M., Camilleri, A. (eds.) FMCAD 1996. LNCS, vol. 1166, pp. 257–264. Springer, Heidelberg (1996). doi: 10.1007/BFb0031813 CrossRefGoogle Scholar
  15. 15.
    Van Den Brand, M.G.J., Heering, J., Klint, P., Olivier, P.A.: Compiling language definitions: the ASF+SDF compiler. ACM Trans. Program. Lang. Syst. 24(4), 334–368 (2002)CrossRefGoogle Scholar
  16. 16.
    Visser, E.: Stratego: a language for program transformation based on rewriting strategies system description of stratego 0.5. In: Middeldorp, A. (ed.) RTA 2001. LNCS, vol. 2051, pp. 357–361. Springer, Heidelberg (2001). doi: 10.1007/3-540-45127-7_27 CrossRefGoogle Scholar
  17. 17.
    Wadler, P.: A prettier printer. In: Gibbons, J., de Moor, O. (eds.) The Fun of Programming (Cornerstones of Computing), Chap. 11, pp. 223–244, Palgrave - Macmillan, March 2003Google Scholar
  18. 18.
    Wenzel, M.: The Isabelle/Isar reference manual, June 2010.
  19. 19.
    Winter, V., Beranek, J.: Program transformation using HATS 1.84. In: Lämmel, R., Saraiva, J., Visser, J. (eds.) GTTSE 2005. LNCS, vol. 4143, pp. 378–396. Springer, Heidelberg (2006). doi: 10.1007/11877028_15 CrossRefGoogle Scholar
  20. 20.
    Woodcock, J., Hughes, A.: Unifying theories of parallel programming. In: George, C., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 24–37. Springer, Heidelberg (2002). doi: 10.1007/3-540-36103-0_5 CrossRefGoogle Scholar
  21. 21.
    Zeyda, F., Cavalcanti, A.: Mechanical reasoning about families of UTP theories. Electr. Notes Theor. Comput. Sci. 240, 239–257 (2009). 10.1016/j.entcs.2009.05.055 CrossRefzbMATHGoogle Scholar

Copyright information

© Springer International Publishing AG 2017

Authors and Affiliations

  1. 1.Trinity College DublinDublinIreland

Personalised recommendations