Predicative Semantics of Loops

  • Theodore S. Norvell
Part of the IFIP Advances in Information and Communication Technology book series (IFIPAICT)


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.


Predicative semantics fixedpoint semantics recursion loops refinement calculi 


  1. 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.Google Scholar
  2. Hehner, Eric C. R., (1979). do considered od: A contribution to the programming calculus. Acta Informatica, 11: 287–304, 1979.zbMATHCrossRefGoogle Scholar
  3. Hehner, Eric C. R., (1984). Predicative programming. Communications of the ACM, 27 (2): 134–151, 1984.zbMATHMathSciNetCrossRefGoogle Scholar
  4. Hehner, Eric C. R., (1993). A Practical Theory of Programming. Springer-Verlag, 1993.zbMATHCrossRefGoogle Scholar
  5. 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.Google Scholar
  6. Hoare, C. A. R and He, JiFeng, , (1987). The weakest prespecification. Information Processing Letters, 24: 127–132, 1987.zbMATHMathSciNetCrossRefGoogle Scholar
  7. 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.Google Scholar
  8. Hoare, C. A. R., (1994). Mathematical models for computer science. Technical report, Oxford University Computing Laboratory, Oxford University, August 1994.Google Scholar
  9. Holt, Richard C., (1991). Healthiness versus realizability in predicate transformers. Technical Report CSRI-240, Computer Systems Research Institute, University of Toronto, 1991.Google Scholar
  10. Morgan, Carroll, (1990). Programming from Specifications. Prentice Hall International, 1990.zbMATHGoogle Scholar
  11. Norvell, Theodore S., (1993). A Predicative Theory of Machine Languages and its Application to Compiler Correctness. PhD thesis, University of Toronto, December 1993.Google Scholar
  12. 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.Google Scholar
  13. Sekerinski, Emil, (1993). A calculus for predicative programming. In Mathematics of Program Construction 1992, number 669 in LNCS, pages 302–322. Springer-Verlag, 1993.Google Scholar
  14. Spivey, J. M., (1989). The Z Notation: A Reference Manual. Prentice-Hall, 1989.zbMATHGoogle Scholar
  15. Tarski, Alfred, (1955). A lattice-theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics, 5: 285–309, 1955.zbMATHMathSciNetCrossRefGoogle Scholar
  16. V. Karger, Burghard and Hoare, C. A. R, (1994). Sequential calculus. Information Processing Letters, 53: 123–131, 1994.CrossRefGoogle Scholar

Copyright information

© IFIP 1997

Authors and Affiliations

  • Theodore S. Norvell
    • 1
  1. 1.Faculty of EngineeringMemorial University of NewfoundlandCanada

Personalised recommendations