×

zbMATH — the first resource for mathematics

Ten years of Hoare’s logic: A survey. II: Nondeterminism. (English) Zbl 0523.68015

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N01 General topics in the theory of software
PDF BibTeX XML Cite
Full Text: DOI
References:
[1] Apt, K.R., Ten years of Hoare’s logic, a survey—part I, Ioplas, 3, 4, 431-483, (1981) · Zbl 0471.68006
[2] Apt, K.R.; Olderog, E.-R., Proof rules and transformations dealing with fairness, (), 3, 1, 1-8, (1983), Extended abstract appeared in: · Zbl 0512.68014
[3] Apt, K.R.; Plotkin, G.D., Countable nondeterminism and random assignment, (), 479-494, extended abstract appeared as: · Zbl 0627.68015
[4] Apt, K.R.; Pnueli, A.; Stavi, J., Fair termination revisited—with delay, Bangalore, India, Proc. 2nd conf. on foundations of software technology and theoretical computer science, 146-170, (1982) · Zbl 0533.68010
[5] De Bakker, J.W., Mathematical theory of program correctness, (1980), Prentice-Hall Englewood Cliffs, NJ
[6] Cook, S.A., Soundness and completeness of an axiom system for program verification, SIAM J. comput., 7, 1, 70-90, (1978) · Zbl 0374.68009
[7] Dijkstra, E.W., Guarded commands, nondeterminancy and formal derivation of programs, Comm. ACM, 18, 8, (1975) · Zbl 0308.68017
[8] Dijkstra, E.W., A discipline of programming, (1976), Prentice-Hall Englewood Cliffs, NJ · Zbl 0286.00013
[9] Floyd, R.W., Nondeterministic algorithms, J. ACM, 14, 4, 636-644, (1967) · Zbl 0153.47006
[10] Grümberg, O.; Francez, N.; Makowsky, J.A.; de Roever, W.P., A proof rule for fair termination of guarded commands, (), 399-416
[11] Harel, D., First-order dynamic logic, () · Zbl 0403.03024
[12] Harel, D.; Kozen, D., A programming lanuage for the inductive sets, and applications, (), 313-329
[13] Hennessy, M.C.B.; Plotkin, G.D., Full abstraction for a simple programming language, (), 108-120 · Zbl 0457.68006
[14] Hoare, C.A.R., An axiomatic basis for computer programming, Comm. ACM, Comm. ACM, 12, 19, 583-580, (1969) · Zbl 0179.23105
[15] Lauer, P.E., Consistent formal theories of the semantics of programming languages, () · Zbl 0264.68006
[16] Lehmann, D., Another proof for the completeness of a rule for the fair termination of guarded commands and another rule for their just termination, ()
[17] Lehmann, D.; Pnueli, A.; Stavi, J., Impartiality, justice and fairness: the ethics of concurrent termination, (), 264-277 · Zbl 0468.68026
[18] Park, D., A predicate transformer for weak fair iteration, ()
[19] Pnueli, A., The temporal semantics of concurrent programs, Theoret. comput. sci., 13, 1, 45-60, (1981) · Zbl 0441.68010
[20] Queille, J.P.; Sifakis, J., Fairness and related properties in transition systems—a temporal logic to deal with fairness, Acta inform., 19, 3, 195-220, (1983) · Zbl 0489.68024
[21] Rogers, H., Theory of recursive functions and effective computability, (1967), McGraw-Hill New York · Zbl 0183.01401
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.