Skip to main content
SpringerLink
Log in

The weakest precondition calculus: Recursion and duality

  • Published:
Formal Aspects of Computing

Abstract

An extension of Dijkstra's guarded command language is studied, including unbounded demonic choice and a backtrack operator. We consider three orderings on this language: a refinement ordering defined by Back, a new deadlock ordering, and an approximation ordering of Nelson. The deadlock ordering is in between the two other orderings. All operators are monotonic in Nelson's ordering, but backtracking is not monotonic in Back's ordering and sequential composition is not monotonic for the deadlock ordering. At first sight recursion can only be added using Nelson's ordering. We show that, under certain circumstances, least fixed points for non-monotonic functions can be obtained by iteration from the least element. This permits the addition of recursion even using Back's ordering or the deadlock ordering in a fully compositional way. In order to give a semantic characterization of the three orderings that relates initial states to possible outcomes of the computation, the relation between predicate transformers and discrete power domains is studied. We consider (two versions of) the Smyth power domain and the Egli-Milner power domain.

This is a preview of subscription content, log in via an institution to check access.

Access this article

Log in via an institution

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Apt, K.R. and Plotkin, G.: A Cook's tour of Countable Nondeterminism. In S. Evens and O. Kariv, editors,Proc. 8th ICALP, Lecture Notes in Computer Science 115, Akko, Israel, 1981. Springer-Verlag.

    Google Scholar 

  2. Apt, K.R. and Plotkin, G.: Countable Nondeterminism and Random Assignment.Journal of the ACM, 33(4):724–767, October 1986.

    Article  MATH  MathSciNet  Google Scholar 

  3. Back, R.-J.R.:On the Correctness of Refinement Steps in Program Development. PhD thesis, Department of Computer Science, University of Helsinki, 1978. Report A-1978-4.

  4. Back, R.-J.R.:Correctness Preserving Program Refinements: Proof Theory and Applications. Mathematical Centre Tracts vol. 131, Mathematical Centre, Amsterdam, 1980.

    Google Scholar 

  5. Back, R.-J.R.: On Correct Refinement of Programs.Journal of Computer and System Sciences, 23(l):49–68, 1981.

    Article  MATH  MathSciNet  Google Scholar 

  6. Back, R.-J.R.: Refinement Calculus, part II: Parallel and Reactive Programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, Lecture Notes in Computer Science 430, pp. 67–93. Springer-Verlag, 1990.

  7. de Bakker, J.W.:Mathematical Theory of Program Correctness. Prentice-Hall, 1980.

  8. Best, E.: Relational Semantic of Concurrent Programs (with some Applications). In D. Bjorner, editor,Proc. of the IFIP Working Conference on on Formal Description of Programming Concepts-II, pp. 431–452, Garmisch-Partenkirchen, FRG, 1983. North-Holland Publishing Company.

  9. Bonsangue, M.M. and Kok, J.N.: Isomorphisms between State and Predicate Transformers. In A.M. Borzyszkowski and S. Sokolowoski, editors,Proc. MFCS '93, Gdansk, Poland, Lecture Notes in Computer Science 711, pp. 301–310. Springer-Verlag, 1993.

  10. Bonsangue, M.M. and Kok, J.N.: The Weakest Precondition Calculus: Recursion and Duality.Formal Aspects of Computing, 6(E): 71–100, 1994.

    Google Scholar 

  11. Back, R.-J.R. and von Wright, J.: Refinement Calculus, part I: Sequential Nondeterministic Programs. In J.W. de Bakker, W.-P. de Roever, and G. Rozenberg, editors,Stepwise Refinement of Distributed Systems: Models, Formalisms, Correctness, Lecture Notes in Computer Science 430, pp. 42–66. Springer-Verlag, 1990.

  12. Dijkstra, E.W. and van Gasteren, A.J.M.: A Simple Fixpoint Argument without the Restriction to Continuity.Acta Informatica, 23:l-7, 1986.

    Article  Google Scholar 

  13. Dijkstra, E.W.:A Discipline of Programming. Prentice-Hall, 1976.

  14. Dijkstra, E.W. and Scholten, C.S.:Predicate Calculus and Program Semantics. Springer-Verlag, New York, 1990.

    Book  MATH  Google Scholar 

  15. Hehner, E.C.R.: do considered od: a Contribution to Programming Calculus.Acta Informatica, 11:287–304, 1979.

    Article  MATH  Google Scholar 

  16. Hesselink, W.H.: Predicate Transformer Semantics of General Recursion.Acta Informatica, 26:309–332, 1989.

    MATH  MathSciNet  Google Scholar 

  17. Hitchcock, P. and Park, D.: Induction Rules and Termination Proofs. In M. Nivat, editor,Proc. 1st ICALP, Rocquencourt, France, 1972. North-Holland.

    Google Scholar 

  18. Meyer, J.-J.Ch:Programming Calculi Based on Fixed Point Transformations: Semantics and Applications. PhD thesis, Vrije Universiteit, Amsterdam, 1985.

    Google Scholar 

  19. Morris, J.: A Theoretical Basis for Stepwise Refinement and the Programming Calculus.Science of Computer Programming, 9:287–306, 1987.

    Article  MATH  MathSciNet  Google Scholar 

  20. Morgan, C.C., Robinson, K.A., and Gardiner, P.H.B.: On the Refinement Calculus. Technical Report PRG-70, Programming Research Group, 1988.

  21. Nelson, G.: A Generalization of Dijkstra's Calculus.ACM Transaction on Programming Languages and Systems, 11(4):517–561, 1989.

    Article  Google Scholar 

  22. Plotkin, G.D.: Dijkstra's Predicate Transformer and Smyth's Powerdomain. InProc. of the Winter School on Abstract Software Specification, Lecture Notes in Computer Science 86, pp. 527–553. Springer-Verlag, 1979.

  23. Plotkin, G.D.: Post-Graduate Lecture Notes in Advanced Domain Theory (incorporating the “Pisa Notes”). Department of Computer Science, Univ. of Edinburgh, 1981.

  24. de Roever, W.P.: Dijkstra's Predicate Transformer, Non-Determinism, Recursion, and Terminations. InProc. 5th MFCS, Lecture Notes in Computer Science 45, pp. 472–481. Springer-Verlag, 1976.

  25. Smyth, M.B.: Power Domains.Journal of Computer and System Sciences, 16(1):23–36, 1978.

    Article  MATH  MathSciNet  Google Scholar 

  26. Smyth, M.B.: Power Domains and Predicate Transformers: A Topological View. In J. Diaz, editor,Proc. 10th ICALP, Lecture Notes in Computer Science 154, pp. 662–675, Barcelona, Spain, 1983. Springer-Verlag.

    Google Scholar 

  27. Wand, M.: A Characterisation of Weakest Preconditions.Journal of Computer and System Sciences, 15:209–212, 1977.

    Article  MATH  MathSciNet  Google Scholar 

  28. von Wright, J.: A Lattice-theoretical Basis for Program Refinement. PhD thesis, Abo Akademi, 1990.

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Vrije Universiteit, De Boelelaan 1081a, 1081, HV Amsterdam, The Netherlands

    Marcello M. Bonsangue

  2. Department of Computer Science, Utrecht University, The Netherlands

    Joost N. Kok

Authors
  1. Marcello M. Bonsangue
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Joost N. Kok
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Marcello M. Bonsangue.

Electronic supplementary material

Rights and permissions

Reprints and permissions

About this article

Check for updates. Verify currency and authenticity via CrossMark

Cite this article

Bonsangue, M.M., Kok, J.N. The weakest precondition calculus: Recursion and duality. Formal Aspects of Computing 6 (Suppl 1), 788–800 (1994). https://doi.org/10.1007/BF01213603

Download citation

  • Received:

  • Accepted:

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/BF01213603

Keywords

Search

Navigation