Abstract
We provide proof rules allowing to deal with two fairness assumptions in the context of Dijkstra's do-od programs. These proof rules are obtained by considering a translated version of the original program which uses random assignment x:=? and admits only fair runs. The proof rules use infinite ordinals and deal with the original programs and not their translated versions.
The full version of this paper is available as Bericht Nr. 8104, Institut für Informatik und Praktische Mathematik, University of Kiel, March 1981, and has been submitted for publication.
This is a preview of subscription content, log in via an institution.
Preview
Unable to display preview. Download preview PDF.
References
APT, K.R. & G.D. PLOTKIN, A Cook's Tour of countable nondeterminism, Technical Report, Department of Computer Science, University of Edinburgh, 1980 (to appear in Proc. ICALP 81).
COUSOT, P., Asynchronous iterative methods for solving a fixed point system of monotone equations in a complete lattice, Rapport de Recherche No 88, L.A.7, Université Scientifique et Medicale de Grenoble, 1977.
EMERSON, E.A. & E.M. CLARKE, Characterizing correctness properties of parallel programs using fixpoints, in: Proc. ICALP 80, Lecture Notes in Computer Science 85, Springer Verlag, pp. 169–181, 1980.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1982 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Apt, K.R., Olderog, ER. (1982). Proof rules dealing with fairness. In: Kozen, D. (eds) Logics of Programs. Logic of Programs 1981. Lecture Notes in Computer Science, vol 131. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0025770
Download citation
DOI: https://doi.org/10.1007/BFb0025770
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-11212-9
Online ISBN: 978-3-540-39047-3
eBook Packages: Springer Book Archive