1. R.-J. R. Back & M. Karttunen (1983): A predicate transformer semantics for statements with multiple exits. Unpublished manuscript. University of Helsinki.
  2. Ralph-Johan Back & Joakim von Wright (1998): Refinement Calculus: A Systematic Introduction. Springer-Verlag, doi:10.1007/978-1-4612-1674-2.
  3. R.J.R. Back (1981): On correct refinement of programs. Journal of Computer and System Sciences 23(1), pp. 49 – 68, doi:10.1016/0022-0000(81)90005-2.
  4. R. Banach, M. Poppleton, C. Jeske & S. Stepney (2007): Engineering and theoretical underpinnings of retrenchment. Science of Computer Programming 67(2-3), pp. 301 – 329, doi:10.1016/j.scico.2007.04.002.
  5. E. Boiten & J. Derrick (1998): IO-Refinement in Z. In: Proc. Third BCS-FACS Northern Formal Methods Workshop, Ilkley, UK.
  6. Flaviu Cristian (1984): Correct and Robust Programs. IEEE Transactions on Software Engineering 10(2), pp. 163–174, doi:10.1109/TSE.1984.5010218.
  7. J. Derrick & E. Boiten (2001): Refinement in Z and Object-Z, Foundations and Advanced Applications. Formal Approaches to Computing and Information Technology. Springer, doi:10.1002/stvr.237.
  8. Edsger W. Dijkstra (1975): Guarded commands, nondeterminacy and formal derivation of programs. Commun. ACM 18(8), pp. 453–457, doi:10.1145/360933.360975.
  9. P. H. B. Gardiner & Carroll Morgan (1993): A single complete rule for data refinement. Formal Aspects of Computing 5(4), pp. 367–382, doi:10.1007/BF01212407.
  10. Paul Gardiner & Carroll Morgan (1991): Data refinement of predicate transformers. Theoretical Computer Science 87(1), pp. 143 – 162, doi:10.1016/0304-3975(91)90029-2.
  11. Intel (2013): Intel® 64 and IA-32 Architectures Software Developer’s Manual, Volume 2 (2A, 2B & 2C): Instruction Set Reference, A-Z. Available at
  12. Bart Jacobs (2001): A Formalisation of Java's Exception Mechanism. In: D. Sands: ESOP '01: Proceedings of the 10th European Symposium on Programming Languages and Systems. Springer-Verlag, London, UK, pp. 284–301, doi:10.1007/3-540-45309-1_19.
  13. Dean Jacobs & David Gries (1985): General correctness: a unification of partial and total correctness. Acta Inf. 22(1), pp. 67–83, doi:10.1007/BF00290146.
  14. Ralph Jeffords, Constance Heitmeyer, Myla Archer & Elizabeth Leonard (2009): A Formal Method for Developing Provably Correct Fault-Tolerant Systems Using Partial Refinement and Composition. In: Ana Cavalcanti & DennisR. Dams: FM 2009: Formal Methods, Lecture Notes in Computer Science 5850. Springer Berlin Heidelberg, pp. 173–189, doi:10.1007/978-3-642-05089-3_12.
  15. Steve King & Carroll Morgan (1995): Exits in the Refinement Calculus. Formal Aspects of Computing 7(1), pp. 54–76, doi:10.1007/BF01214623.
  16. K. Rustan M. Leino & Jan L. A. van de Snepscheut (1994): Semantics of Exceptions. In: Ernst-Rüdiger Olderog: PROCOMET '94: Proceedings of the IFIP TC2/WG2.1/WG2.2/WG2.3 Working Conference on Programming Concepts, Methods and Calculi, IFIP Transactions A-56. North-Holland Publishing Co., pp. 447–466. Available at
  17. Rajit Manohar & K. Rustan M. Leino (1995): Conditional Composition. Formal Aspects of Computing 7(6), pp. 683–703, doi:10.1007/BF01211001.
  18. Bertrand Meyer (1997): Object-Oriented Software Construction, 2nd edition. Prentice-Hall, Inc..
  19. Microsoft (2013): NotImplementedException Class. Available at
  20. Microsoft (2013): OverflowException Class. Available at
  21. Anna Mikhajlova & Emil Sekerinski (1997): Class Refinement and Interface Refinement in Object-Oriented Programs. In: John Fitzgerald, Cliff Jones & Peter Lucas: FME '97: Industrial Applications and Strengthened Foundations of Formal Methods, Lecture Notes in Computer Science 1313. Springer-Verlag, pp. 82–101, doi:10.1007/3-540-63533-5_5.
  22. David L. Parnas (1978): Designing software for ease of extension and contraction. In: Proceedings of the 3rd international conference on Software engineering, ICSE '78. IEEE Press, Piscataway, NJ, USA, pp. 264–277, doi:10.1109/TSE.1979.234169.
  23. Emil Sekerinski & Tian Zhang (2011): A New Notion of Partial Correctness for Exception Handling. In: Borzoo Bonakdarpour & Tom Maibaum: Proceedings of the 2nd International Workshop on Logical Aspects of Fault-Tolerance, pp. 116–132. Available at
  24. Susan Stepney, David Cooper & Jim Woodcock (1998): More Powerful Z Data Refinement: Pushing the State of the Art in Industrial Refinement. In: Jonathan P. Bowen, Andreas Fett & Michael G. Hinchey: ZUM '98: The Z Formal Specification Notation, Lecture Notes in Computer Science 1493. Springer Berlin Heidelberg, pp. 284–307, doi:10.1007/978-3-540-49676-2_20.
  25. G. Watson (2002): Refining exceptions using King and Morgan's exit construct. In: Software Engineering Conference, 2002. Ninth Asia-Pacific, pp. 43–51, doi:10.1109/APSEC.2002.1182974.
  26. J. von Wright (1994): The lattice of data refinement. Acta Informatica 31(2), pp. 105–135, doi:10.1007/BF01192157.

Comments and questions to:
For website issues: