Another characterization of weakest preconditions

  • Pedro Guerreiro
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 137)


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.


Binary Relation Semantic Relation Total Correctness Programmable Relation Note Comp 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. (Bac 79).
    R.-J,Back, "Semantics of unbounded nondeterminism". Proceedings ICALP 80, Lect. Notes Comp. Sci. 85, Springer (1980).Google Scholar
  2. (Dij 75).
    E.W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs". CACM 18,8 (August 1975), pp. 453–457.Google Scholar
  3. (Dij 76).
    E.W.Dijkstra, "A Discipline of Programming". Prentice Hall (1976).Google Scholar
  4. (Gue 80).
    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. (Gue 81).
    P.Guerreiro,"Semantique Relationnelle des Programmes Non-deterministes et des Processus Communicants". These de зeme Cycle, Univ. Grenoble I, (July 1981).Google Scholar
  6. (Har 79).
    D.Harel, "On the total correctness of nondeterministic programs". IBM Research Report RC7691 (1979).Google Scholar
  7. (Hoa 78).
    C.A.R. Hoare, "Some properties of predicate transformers". JACM 25,3 (July 1978), pp. 461–480.Google Scholar
  8. (Roe 76).
    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. (Sif 79).
    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. (Wan 77).
    M. Wand, "A characterization of weakest preconditions". Journal of Computer and Systems Sciences 15, (1977), pp. 209–212.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1982

Authors and Affiliations

  • Pedro Guerreiro
    • 1
  1. 1.Departamento de Informática Faculdade de Ciências e TecnologiaUniversidade Nova de LisboaMonte da CaparicaPortugal

Personalised recommendations