Ten years of Hoare's logic: A survey. II: Nondeterminism

DOI10.1016/0304-3975(83)90066-XzbMath0523.68015OpenAlexW2063825888MaRDI QIDQ1056534

Krzysztof R. Apt

Publication date: 1984

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/0304-3975(83)90066-x

zbMATH Keywords

fairnesscompletenesssoundnesspartial correctnesstotal correctnessbounded nondeterminismcountable nondeterminismfreedom of failure

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) General topics in the theory of software (68N01)

Related Items (21)

The Hoare Logic of Deterministic and Nondeterministic Monadic Recursion Schemes ⋮ Process algebra with guards: Combining hoare logic with process algebra ⋮ The origins of structural operational semantics ⋮ A complete rule for equifair termination ⋮ Being and Change: Reasoning About Invariance ⋮ Rewriting with a nondeterministic choice operator ⋮ Modeling Actor Systems Using Dynamic I/O Automata ⋮ On the programs-as-formulas interpretation of parallel programs in Peano arithmetic ⋮ Hoare Logic for Disjunctive Information Flow ⋮ A language independent proof of the soundness and completeness of generalized Hoare logic ⋮ Completeness of Hoare Logic Relative to the Standard Model ⋮ Observable behavior of distributed systems: component reasoning for concurrent objects ⋮ Synthesis of Strategies Using the Hoare Logic of Angelic and Demonic Nondeterminism ⋮ Linking operational semantics and algebraic semantics for a probabilistic timed shared-variable language ⋮ Process expressions and Hoare's logic: Showing and irreconcilability of context-free recursion with Scott's induction rule ⋮ Content dependent information flow control ⋮ Verification of concurrent programs: The automata-theoretic framework ⋮ Fifty years of Hoare's logic ⋮ Reverse Hoare Logic ⋮ Hoare's logic for nondeterministic regular programs: A nonstandard approach ⋮ Observable Behavior of Dynamic Systems: Component Reasoning for Concurrent Objects

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Proof rules and transformations dealing with fairness
• The temporal semantics of concurrent programs
• Fairness and related properties in transition systems - a temporal logic to deal with fairness
• First-order dynamic logic
• Consistent and complementary formal theories of the semantics of programming languages
• Countable nondeterminism and random assignment
• Ten Years of Hoare's Logic: A Survey—Part I
• Guarded commands, nondeterminacy and formal derivation of programs
• Soundness and Completeness of an Axiom System for Program Verification
• Programming as a Discipline of Mathematical Nature
• Nondeterministic Algorithms
• An axiomatic basis for computer programming

This page was built for publication: Ten years of Hoare's logic: A survey. II: Nondeterminism