Abstract
We study a propositional variant of Hoare logic that can be used for reasoning about programs that exhibit both angelic and demonic nondeterminism. We work in an uninterpreted setting, where the meaning of the atomic actions is specified axiomatically using hypotheses of a certain form. Our logical formalism is entirely compositional and it subsumes the non-compositional formalism of safety games on finite graphs. We present sound and complete Hoare-style (partial-correctness) calculi that are useful for establishing Hoare assertions, as well as for synthesizing implementations. The computational complexity of the Hoare theory of dual nondeterminism is investigated using operational models, and it is shown that the theory is complete for exponential time.
Part of the present work was done while visiting Radboud University Nijmegen.
Chapter PDF
Similar content being viewed by others
Keywords
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.
References
Back, R.-J., Wright, J.: Refinement Calculus: A Systematic Introduction. Springer, Heidelberg (1998)
Celiku, O., Wright, J.v.: Implementing angelic nondeterminism. In: Tenth Asia-Pacific Software Engineering Conference, pp. 176–185 (2003)
Cook, S.A.: Soundness and completeness of an axiom system for program verification. SIAM Journal on Computing 7(1), 70–90 (1978)
Dijkstra, E.W.: Guarded commands, nondeterminacy and formal derivation of programs. Communications of the ACM 18(8), 453–457 (1975)
Hoare, C.A.R.: An axiomatic basis for computer programming. Communications of the ACM 12(10), 576–580 (1969)
Kozen, D.: On Hoare logic and Kleene algebra with tests. ACM Transactions on Computational Logic 1(1), 60–76 (2000)
Mamouras, K.: The Hoare logic of deterministic and nondeterministic monadic recursion schemes (2014) (manuscript)
Mamouras, K.: On the Hoare theory of monadic recursion schemes. In: Proceedings of CSL-LICS (2014)
Mamouras, K.: Synthesis of strategies using the Hoare logic of angelic and demonic nondeterminism (2015) (in preparation)
Martin, C.E., Curtis, S.A., Rewitzky, I.: Modelling nondeterminism. In: Mathematics of Program Construction, pp. 228–251 (2004)
Morgan, C.: Programming From Specifications. Prentice-Hall (1998)
Pauly, M., Parikh, R.: Game logic — An overview. Studia Logica 75(2), 165–182 (2003)
Rewitzky, I.: Binary multirelations. In: de Swart, H., Orłowska, E., Schmidt, G., Roubens, M. (eds.) TARSKI. LNCS, vol. 2929, pp. 256–271. Springer, Heidelberg (2003)
Thomas, W.: On the synthesis of strategies in infinite games. In: Mayr, E.W., Puech, C. (eds.) STACS 1995. LNCS, vol. 900, pp. 1–13. Springer, Heidelberg (1995)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2015 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Mamouras, K. (2015). Synthesis of Strategies and the Hoare Logic of Angelic Nondeterminism. In: Pitts, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2015. Lecture Notes in Computer Science(), vol 9034. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-46678-0_2
Download citation
DOI: https://doi.org/10.1007/978-3-662-46678-0_2
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-662-46677-3
Online ISBN: 978-3-662-46678-0
eBook Packages: Computer ScienceComputer Science (R0)