Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic

DOI10.1016/0304-3975(80)90005-5zbMath0433.68019OpenAlexW2021907707MaRDI QIDQ1139368

David Harel

Publication date: 1980

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

Full work available at URL: https://doi.org/10.1016/0304-3975(80)90005-5

zbMATH Keywords

dynamic logicterminationweakest preconditioncorrectness of programsintermittent assertion methoddeterministic while programsinvariant assertion method

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Abstract data types; algebraic specification (68Q65)

Related Items (3)

An observationally complete program logic for imperative higher-order functions ⋮ Nondeterministic flowchart programs with recursive procedures: Semantics and correctness. II ⋮ Semantics of algorithmic languages

Cites Work

• On the total correctness of nondeterministic programs
• A closer look at termination
• On the completeness of the inductive assertion method
• Axioms for total correctness
• First-order dynamic logic
• Automatic program verification. I: A logical basis and its implementation
• Axiomatic approach to total correctness of programs
• And/Or Programs: A New Approach to Structured Programming
• Guarded commands, nondeterminacy and formal derivation of programs
• An axiomatic basis for proving total correctness of goto-programs
• Verifying properties of parallel programs
• Proof Theory of Partial Correctness Verification Systems
• Subgoal induction
• Logical analysis of programs
• Lucid—A Formal System for Writing and Proving Programs
• Is “sometime” sometimes better than “always”?
• Soundness and Completeness of an Axiom System for Program Verification
• Some Properties of Predicate Transformers
• Programming as a Discipline of Mathematical Nature
• An axiomatic basis for computer programming
• Algorithmic properties of structures
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: Proving the correctness of regular deterministic programs: A unifying survey using dynamic logic