Abstract
A predicative semantics is a mapping of programs to predicates. These predicates characterize sets of acceptable observations. The presence of time in the observations makes the obvious weakest fixed-point semantics of iterative constructs unacceptable. This paper proposes an alternative. We will see that this alternative semantics is monotone and implementable (feasible). Finally a programming theorem for iterative constructs is proposed, proved, and demonstrated. A novel aspect of this theorem is that it is not based on invariants.
Chapter PDF
Similar content being viewed by others
References
Back, R. J. R. and von Wright, J., (1990). Refinement calculus, part 1: Sequential nondeterministic programs. In de Backer, J. W., de Roever, W.-P., and Rosenberg, G., editors, Stepwise Refinement of Distributed Systems: Models Formalisms, Correctness, number 430 in Lecture Notes in Computer Science. Springer-Verlag, 1990.
Hehner, Eric C. R., (1979). do considered od: A contribution to the programming calculus. Acta Informatica, 11: 287–304, 1979.
Hehner, Eric C. R., (1984). Predicative programming. Communications of the ACM, 27 (2): 134–151, 1984.
Hehner, Eric C. R., (1993). A Practical Theory of Programming. Springer-Verlag, 1993.
Hehner, Eric C. R., (1994). Abstractions of time. In Roscoe, A. W., editor, A Classical Mind, chapter 12, pages 195–214. Prentice-Hall International, 1994.
Hoare, C. A. R and He, JiFeng, , (1987). The weakest prespecification. Information Processing Letters, 24: 127–132, 1987.
Hoare, C. A. R., (1985). Programs are predicates. In Hoare, C. A. R. and Shepherdson, J. C., editors, Mathematical Logic and Programming Languages, pages 141–155. Prentice Hall, 1985.
Hoare, C. A. R., (1994). Mathematical models for computer science. Technical report, Oxford University Computing Laboratory, Oxford University, August 1994.
Holt, Richard C., (1991). Healthiness versus realizability in predicate transformers. Technical Report CSRI-240, Computer Systems Research Institute, University of Toronto, 1991.
Morgan, Carroll, (1990). Programming from Specifications. Prentice Hall International, 1990.
Norvell, Theodore S., (1993). A Predicative Theory of Machine Languages and its Application to Compiler Correctness. PhD thesis, University of Toronto, December 1993.
Norvell, Theodore S., (1994). Machine code programs are predicates too. In Till, David, editor, Sixth Refinement Workshop, Workshops in Computing, pages 188–204. Springer Verlag, 1994.
Sekerinski, Emil, (1993). A calculus for predicative programming. In Mathematics of Program Construction 1992, number 669 in LNCS, pages 302–322. Springer-Verlag, 1993.
Spivey, J. M., (1989). The Z Notation: A Reference Manual. Prentice-Hall, 1989.
Tarski, Alfred, (1955). A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5: 285–309, 1955.
V. Karger, Burghard and Hoare, C. A. R, (1994). Sequential calculus. Information Processing Letters, 53: 123–131, 1994.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1997 IFIP
About this chapter
Cite this chapter
Norvell, T.S. (1997). Predicative Semantics of Loops. In: Bird, R.S., Meertens, L. (eds) Algorithmic Languages and Calculi. IFIP Advances in Information and Communication Technology. Springer, Boston, MA. https://doi.org/10.1007/978-0-387-35264-0_16
Download citation
DOI: https://doi.org/10.1007/978-0-387-35264-0_16
Publisher Name: Springer, Boston, MA
Print ISBN: 978-1-5041-2877-3
Online ISBN: 978-0-387-35264-0
eBook Packages: Springer Book Archive