Skip to main content
SpringerLink
Log in

Another characterization of weakest preconditions

  • Conference paper
  • First Online:
International Symposium on Programming (Programming 1982)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 137))

Included in the following conference series:

Abstract

We present an approach to the study of nondeterministic programs, consisting essentially in using binary relations as semantic objects representing the input-output behaviour of programs. These relations include an explicit representation of non-terminating computations. Based on the relational model we introduce a weakest precondition total correctness predicate transformer. We then show how to build up this predicate transformer starting from others of a more elementar kind. Finally,we obtain a characterization of its healthiness properties in terms of set-theoretical properties of the relations involved.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. R.-J,Back, "Semantics of unbounded nondeterminism". Proceedings ICALP 80, Lect. Notes Comp. Sci. 85, Springer (1980).

    Google Scholar 

  2. E.W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs". CACM 18,8 (August 1975), pp. 453–457.

    Google Scholar 

  3. E.W.Dijkstra, "A Discipline of Programming". Prentice Hall (1976).

    Google Scholar 

  4. P. Guerreiro, "A relational model for nondeterministic programs and predicate transformers". Fourth International Colloquium on Programming, Paris, Lect. Notes Comp. Sci. 83, Springer (1980), pp. 136–146.

    Google Scholar 

  5. P.Guerreiro,"Semantique Relationnelle des Programmes Non-deterministes et des Processus Communicants". These de зeme Cycle, Univ. Grenoble I, (July 1981).

    Google Scholar 

  6. D.Harel, "On the total correctness of nondeterministic programs". IBM Research Report RC7691 (1979).

    Google Scholar 

  7. C.A.R. Hoare, "Some properties of predicate transformers". JACM 25,3 (July 1978), pp. 461–480.

    Google Scholar 

  8. W.P. de Roever, "Dijkstra's predicate transformer, non-determinism, recursion and termination". Math. Found. Comp. Sci. 1976, Lect. Notes Comp. Sci. 45, Springer (1976), pp.472–481.

    Google Scholar 

  9. J.Sifakis. "A unified approach for studying properties of transition systems". Rapport de Recherche 179, IMAG, Grenoble, (December 1979). To appear in Theoretical Computer Science.

    Google Scholar 

  10. M. Wand, "A characterization of weakest preconditions". Journal of Computer and Systems Sciences 15, (1977), pp. 209–212.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Departamento de Informática Faculdade de Ciências e Tecnologia, Universidade Nova de Lisboa, Quinta da Torre, 2825, Monte da Caparica, Portugal

    Pedro Guerreiro

Authors
  1. Pedro Guerreiro
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Mariangiola Dezani-Ciancaglini Ugo Montanari

Rights and permissions

Reprints and permissions

Copyright information

© 1982 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Guerreiro, P. (1982). Another characterization of weakest preconditions. In: Dezani-Ciancaglini, M., Montanari, U. (eds) International Symposium on Programming. Programming 1982. Lecture Notes in Computer Science, vol 137. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-11494-7_12

Download citation

  • DOI: https://doi.org/10.1007/3-540-11494-7_12

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-11494-9

  • Online ISBN: 978-3-540-39184-5

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation