Another characterization of weakest preconditions
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.
KeywordsBinary Relation Semantic Relation Total Correctness Programmable Relation Note Comp
Unable to display preview. Download preview PDF.
- (Bac 79).R.-J,Back, "Semantics of unbounded nondeterminism". Proceedings ICALP 80, Lect. Notes Comp. Sci. 85, Springer (1980).Google Scholar
- (Dij 75).E.W. Dijkstra, "Guarded commands, nondeterminacy and formal derivation of programs". CACM 18,8 (August 1975), pp. 453–457.Google Scholar
- (Dij 76).E.W.Dijkstra, "A Discipline of Programming". Prentice Hall (1976).Google Scholar
- (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
- (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
- (Har 79).D.Harel, "On the total correctness of nondeterministic programs". IBM Research Report RC7691 (1979).Google Scholar
- (Hoa 78).C.A.R. Hoare, "Some properties of predicate transformers". JACM 25,3 (July 1978), pp. 461–480.Google Scholar
- (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
- (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
- (Wan 77).M. Wand, "A characterization of weakest preconditions". Journal of Computer and Systems Sciences 15, (1977), pp. 209–212.Google Scholar