Skip to main content
Conference ProceedingsOPEN ACCESS

A relational model for non-deterministic programs and predicate transformers

Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (1980) 83 LNCS 136-146
DOI: 10.1007/3-540-09981-6_10
6Citations
Citations of this article
2Readers
Mendeley users who have this article in their library.

This article is free to access.

Abstract

A relational model for non-deterministic programs is presented. Several predicate transformers are introduced and it is shown that one of them satisfies all the healthiness criteria indicated by Dijkstra for a useful total correctness predicate transformer. An axiomatic relational definition of the language of guarded commands is proposed. From it the predicate transformers associated to each command in the language are derived. The fact that Dijkstra's axioms are rediscovered proves their consistency in the model.

Cite

CITATION STYLE

APA

Guerreiro, P. (1980). A relational model for non-deterministic programs and predicate transformers. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 83 LNCS, pp. 136–146). Springer Verlag. https://doi.org/10.1007/3-540-09981-6_10

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free