Abstract
We present a novel Hoare-style logic, called Reverse Hoare Logic, which can be used to reason about state reachability of imperative programs. This enables us to give natural specifications to randomized (deterministic or nondeterministic) algorithms. We give a proof system for the logic and use this to give simple formal proofs for a number of illustrative examples. We define a weakest postcondition calculus and use this to show that the proof system is sound and complete. © 2011 Springer-Verlag.
Cite
CITATION STYLE
De Vries, E., & Koutavas, V. (2011). Reverse hoare logic. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 7041 LNCS, pp. 155–171). https://doi.org/10.1007/978-3-642-24690-6_12
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
