Theories, Implementations, and Transformations

  • Eric Hehner
  • Ioannis T. Kassios
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2272)


The purpose of this paper is to try to put theory presentation and structuring in the simplest possible logical setting in order to improve our understanding of it. We look at how theories can be combined, and compared for strength. We look at theory refinement and implementation, and what constitutes proof of correctness. Our examples come from both the functional style and imperative (state-changing) style of theory. Finally, we explore how one implementation can be transformed to another.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    J.-R. Abrial: the B book, Assigning Programs to Meanings, Cambridge University Press, 1996Google Scholar
  2. 2.
    R.M. Burstall, J.A. Goguen: “Putting Theories Together to make Specifications”, in R. Reddy ed.: Proceedings of the fifth International Joint Conference on Artificial Intelligence, volume 6 pages 1045–1058, Morgan Kaufman, Cambridge MA, 1977Google Scholar
  3. 3.
    P.H.B. Gardiner, C.C. Morgan: “a Single Complete Rule for Data Refinement”, Formal Aspects of Computing, volume 5 number 4 pages 367–382, 1993zbMATHCrossRefGoogle Scholar
  4. 4.
    J.V. Guttag, J.J. Horning: “the Algebraic Specification of Abstract Data Types”, Acta Informatica, volume 10 pages 27–52, 1978zbMATHCrossRefMathSciNetGoogle Scholar
  5. 5.
    E.C.R. Hehner: a Practical Theory of Programming, second edition, Springer, 2002Google Scholar
  6. 6.
    I.T. Kassios: Theory Theory and an Attempt to Orient Objections to Object Orientation, MSc thesis, University of Toronto, 2001Google Scholar
  7. 7.
    W.-P. de Roever, K. Engelhardt: Data Refinement: Model-Oriented Proof Methods and their Comparisons, tracts in Theoretical Computer Science volume 47, Cambridge University Press, 1998Google Scholar
  8. 8.
    J.M. Spivey: Introducing Z: a Specification Language and its Formal Semantics, Cambridge University Press, 1988Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2002

Authors and Affiliations

  • Eric Hehner
    • 1
  • Ioannis T. Kassios
    • 1
  1. 1.Department of Computer ScienceUniversity of TorontoTorontoCanada

Personalised recommendations