Theories, Implementations, and Transformations
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.
- 1.J.-R. Abrial: the B book, Assigning Programs to Meanings, Cambridge University Press, 1996Google Scholar
- 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
- 5.E.C.R. Hehner: a Practical Theory of Programming, second edition, Springer, 2002Google Scholar
- 6.I.T. Kassios: Theory Theory and an Attempt to Orient Objections to Object Orientation, MSc thesis, University of Toronto, 2001Google Scholar
- 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.J.M. Spivey: Introducing Z: a Specification Language and its Formal Semantics, Cambridge University Press, 1988Google Scholar