Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Unifying Theories of Programming

UTP 2016: Unifying Theories of Programming pp 197–216Cite as

UTPCalc — A Calculator for UTP Predicates

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 10134))

Abstract

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.

A. Butterfield—This work was supported, in part, by Science Foundation Ireland grant 10/CE/I1855 to Lero - the Irish Software Engineering Research Centre (www.lero.ie).

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as EPUB and PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

References

  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

    Book  Google Scholar 

  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)

    Book  MATH  Google Scholar 

  3. Bird, R.: Thinking Functionally with Haskell. Cambridge University Press, Cambridge (2014)

    Book  Google Scholar 

  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). http://dx.doi.org/10.1007/978-3-642-16690-7_6

  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). http://dx.doi.org/10.1007/978-3-642-35705-3_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 2016

    Google Scholar 

  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

    Chapter  Google Scholar 

  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). http://dx.doi.org/10.3233/978-1-61499-495-4-246

  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. 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. http://www.cs.chalmers.se/~rjmh/Papers/pretty.ps

    Chapter  Google Scholar 

  11. Marlow, S. (ed.): Haskell 2010 Language Report. Haskell Community (2010). https://www.haskell.org/definition/haskell2010.pdf

  12. Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL – A Proof Assistant for Higher-Order Logic. LNCS, vol. 2283. Springer, Heidelberg (2002). http://link.springer.de/link/service/series/0558/tocs/t2283.htm

    MATH  Google Scholar 

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  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)

    Article  Google Scholar 

  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

    Chapter  Google Scholar 

  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 2003

    Google Scholar 

  18. Wenzel, M.: The Isabelle/Isar reference manual, June 2010. http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/isar-ref.pdf

  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

    Chapter  Google Scholar 

  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

    Chapter  Google Scholar 

  21. Zeyda, F., Cavalcanti, A.: Mechanical reasoning about families of UTP theories. Electr. Notes Theor. Comput. Sci. 240, 239–257 (2009). http://dx.doi.org/ 10.1016/j.entcs.2009.05.055

    Article  MATH  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Trinity College Dublin, Dublin, Ireland

    Andrew Butterfield

Authors
  1. Andrew Butterfield
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Andrew Butterfield .

Editor information

Editors and Affiliations

  1. London South Bank University, London, United Kingdom

    Jonathan P. Bowen

  2. East China Normal University, Shanghai, China

    Huibiao Zhu

Rights and permissions

Reprints and permissions

Copyright information

© 2017 Springer International Publishing AG

About this paper

Cite this paper

Butterfield, A. (2017). UTPCalc — A Calculator for UTP Predicates. In: Bowen, J., Zhu, H. (eds) Unifying Theories of Programming. UTP 2016. Lecture Notes in Computer Science(), vol 10134. Springer, Cham. https://doi.org/10.1007/978-3-319-52228-9_10

Download citation

  • DOI: https://doi.org/10.1007/978-3-319-52228-9_10

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-319-52227-2

  • Online ISBN: 978-3-319-52228-9

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation