Get the latest tech news
The Hoare Cube
I wrote earlier this year about my attempt to understand the repercussions of toggling $latex \subseteq$ and $latex \supseteq$ when giving a semantics to Hoare triples. In response to that post, Ya…
Name(s)Meaning of ReachDirectionApproximation Partial correctness [1]mayforwardoverReverse Hoare logic [5],Incorrectness logic [6]mayforwardunderNecessary preconditions (as formulated in [4])maybackwardoverBackward under-approximate Hoare triple [2],Lisbon triple [3],Sufficient incorrectness logic [4]maybackwardunderNecessary preconditions (as originally formulated in [7])mustforwardovermustforwardunderPartial correctness (alternative formulation)mustbackwardovermustbackwardunderNote that partial correctness can also be rewritten into the more familiar if we define as the “weakest liberal precondition” in the usual way… [3] Noam Zilberstein, Derek Dreyer, and Alexandra Silva: Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. [11] Petar Maksimovic, Caroline Cronjäger, Andreas Lööw, Julian Sutherland, and Philippa Gardner: Exact Separation Logic: Towards Bridging the Gap Between Verification and Bug-Finding.
Or read this on Hacker News