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. © 2013 Springer-Verlag.
CITATION STYLE
Foster, S., & Woodcock, J. (2013). Unifying theories of programming in Isabelle. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 8050 LNCS, pp. 109–155). https://doi.org/10.1007/978-3-642-39721-9_3
Mendeley helps you to discover research relevant for your work.