| Summary: | 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 calculi that are useful for establishing partial-correctness
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.
|
|---|