Abstract
This is a tutorial introduction to the two most basic theories in Hoare & He’s Unifying Theories of Programming and their mechanisation in the Isabelle interactive theorem prover. We describe the theories of relations and of designs (pre-postcondition pairs), interspersed with their formalisation in Isabelle and example mechanised proofs.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
References
Abrial, J.-R.: The B-Book: Assigning Progams to Meanings. Cambridge University Press (1996)
Back, R.J.R., Wright, J.: Refinement Calculus: A Systematic Introduction. Graduate Texts in Computer Science. Springer (1998)
Blanchette, J.C., Nipkow, T.: Nitpick: A counterexample generator for higher-order logic based on a relational model finder. In: Kaufmann, M., Paulson, L.C. (eds.) ITP 2010. LNCS, vol. 6172, pp. 131–146. Springer, Heidelberg (2010)
Blanchette, J.C., Bulwahn, L., Nipkow, T.: Automatic Proof and Disproof in Isabelle/HOL. In: Tinelli, C., Sofronie-Stokkermans, V. (eds.) FroCoS 2011. LNCS, vol. 6989, pp. 12–27. Springer, Heidelberg (2011) §
Butterfield, A., Sherif, A., Woodcock, J.: Slotted-Circus. In: Davies, J., Gibbons, J. (eds.) IFM 2007. LNCS, vol. 4591, pp. 75–97. Springer, Heidelberg (2007)
Beg, A., Butterfield, A.: Linking a state-rich process algebra to a state-free algebra to verify software/hardware implementation. In: Proceedings of the 8th International Conference on Frontiers of Information Technology, FIT 2010, article 47 (2010)
Cavalcanti, A., Woodcock, J.: A tutorial introduction to CSP in Unifying Theories of Programming. In: Cavalcanti, A., Sampaio, A., Woodcock, J. (eds.) PSSE 2004. LNCS, vol. 3167, pp. 220–268. Springer, Heidelberg (2006)
Cavalcanti, A., Sampaio, A., Woodcock, J.: Unifying classes and processes. Software and System Modeling 4(3), 277–296 (2005)
de Moura, L., Bjørner, N.: Z3: An efficient SMT solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Feliachi, A., Gaudel, M.-C., Wolff, B.: Isabelle/Circus: A Process Specification and Verification Environment. In: Joshi, R., Müller, P., Podelski, A. (eds.) VSTTE 2012. LNCS, vol. 7152, pp. 243–260. Springer, Heidelberg (2012)
Harwood, W., Cavalcanti, A., Woodcock, J.: A theory of pointers for the UTP. In: Fitzgerald, J.S., Haxthausen, A.E., Yenigun, H. (eds.) ICTAC 2008. LNCS, vol. 5160, pp. 141–155. Springer, Heidelberg (2008)
Hehner, E.C.R.: Retrospective and prospective for Unifying Theories of Programming. In: Dunne, S., Stoddart, B. (eds.) UTP 2006. LNCS, vol. 4010, pp. 1–17. Springer, Heidelberg (2006)
Hillenbrand, T., Buch, A., Vogt, R., Löchner, B.: Waldmeister: High-performance equational deduction. Journal of Automated Reasoning 18(2), 265–270 (1997)
Hoare, C.A.R.: Communicating Sequential Processes. Prentice-Hall (1985)
Hoare, C.A.R., He, J.: Unifying Theories of Programming. Series in Computer Science. Prentice Hall (1998)
Jones, C.B.: Systematic Software Development Using VDM. Prentice-Hall International (1986)
Morgan, C.: Programming from Specifications, 2nd edn. Prentice-Hall (1994)
Morris, J.M.: A Theoretical Basis for Stepwise Refinement and the Programming Calculus. Science of Computer Programming 9(3), 287–306 (1987)
Nipkow, T., Paulson, L.C., Wenzel, M.: Isabelle/HOL. LNCS, vol. 2283. Springer, Heidelberg (2002)
Oliveira, M.V.M.: Formal derivation of state-rich reactive programs using Circus. PhD Thesis, Department of Computer Science, University of York, Report YCST-2006/02 (2005)
Oliveira, M., Cavalcanti, A., Woodcock, J.: A UTP semantics for Circus. Formal Asp. Comput. 21(1-2), 3–32 (2009)
Oliveira, M., Cavalcanti, A., Woodcock, J.: Unifying theories in ProofPower-Z. Formal Aspects of Computing 25(1), 133–158 (2013)
Perna, J.I., Woodcock, J.: UTP semantics for Handel-C. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 142–160. Springer, Heidelberg (2010)
Riazanov, A., Voronkov, A.: The design and implementation of Vampire. Journal of AI Communications 15(2/3), 91–110 (2002)
Sampaio, A., Woodcock, J., Cavalcanti, A.: Refinement in Circus. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 451–470. Springer, Heidelberg (2002)
Schultz, S.: E—A braniac theorem prover. Journal of AI Communications 15(2/3), 111–126 (2002)
Sherif, A., He, J.: Towards a Time Model for Circus. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 613–624. Springer, Heidelberg (2002)
Michael Spivey, J.: The Z Notation: A Reference Manual, 2nd edn. Series in Computer Science. Prentice Hall International (1992)
Tang, X., Woodcock, J.: Towards Mobile Processes in Unifying Theories. In: 2nd International Conference on Software Engineering and Formal Methods (SEFM 2004), Beijing, China, September 28–30, pp. 44–53. IEEE Computer Society (2004)
Tang, X., Woodcock, J.: Travelling Processes. In: Kozen, D., Shankland, C. (eds.) MPC 2004. LNCS, vol. 3125, pp. 381–399. Springer, Heidelberg (2004)
Wei, K., Woodcock, J., Cavalcanti, A.: Circus Time with Reactive Designs. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 68–87. Springer, Heidelberg (2013)
Weidenbach, C., Dimova, D., Fietzke, A., Kumar, R., Suda, M., Wischnewski, P.: SPASS Version 3.5. In: Schmidt, R.A. (ed.) CADE 2009. LNCS, vol. 5663, pp. 140–145. Springer, Heidelberg (2009)
Woodcock, J., Davies, J.: Using Z—Specification, Refinement, and Proof. Prentice-Hall (1996)
Woodcock, J., Cavalcanti, A.: A Concurrent Language for Refinement. In: Butterfield, A., Strong, G., Pahl, C. (eds.) 5th Irish Workshop on Formal Methods, IWFM 2001, Dublin, Ireland, July 16–17. BCS Workshops in Computing, pp. 16–17 (2001)
Woodcock, J., Cavalcanti, A.: The Semantics of Circus. In: Bert, D., Bowen, J.P., Henson, M.C., Robinson, K. (eds.) ZB 2002. LNCS, vol. 2272, pp. 184–203. Springer, Heidelberg (2002)
Woodcock, J., Cavalcanti, A.: A tutorial introduction to Designs in Unifying Theories of Programming. In: Boiten, E.A., Derrick, J., Smith, G. (eds.) IFM 2004. LNCS, vol. 2999, pp. 40–66. Springer, Heidelberg (2004)
Woodcock, J., Cavalcanti, A., Fitzgerald, J., Larsen, P., Miyazawa, A., Perry, S.: Features of CML: A formal modelling language for Systems of Systems. In: 7th IEEE International Conference on System of Systems Engineering (SoSE), pp. 1–6 (2012)
Zhan, N., Kang, E.Y., Liu, Z.: Component publications and compositions. In: Butterfield, A. (ed.) UTP 2008. LNCS, vol. 5713, pp. 238–257. Springer, Heidelberg (2010)
Zhu, H., Yang, F., He, J.: Generating denotational semantics from algebraic semantics for event-driven system-level language. In: Qin, S. (ed.) UTP 2010. LNCS, vol. 6445, pp. 286–308. Springer, Heidelberg (2010)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2013 Springer-Verlag Berlin Heidelberg
About this chapter
Cite this chapter
Foster, S., Woodcock, J. (2013). Unifying Theories of Programming in Isabelle. In: Liu, Z., Woodcock, J., Zhu, H. (eds) Unifying Theories of Programming and Formal Engineering Methods. Lecture Notes in Computer Science, vol 8050. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-39721-9_3
Download citation
DOI: https://doi.org/10.1007/978-3-642-39721-9_3
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-39720-2
Online ISBN: 978-3-642-39721-9
eBook Packages: Computer ScienceComputer Science (R0)