The traditional Hoare logic is the "partial correctness" form - if the program state satisfies a precondition, and executing the program terminates with some other state, then the second state satisfies the postcondition. This is "correctness" in the sense it overapproximates all executions: if the postcondition says something about the state being "good", the precondition ensures you end in a "good" state, but perhaps there are more "good" states than actually reachable ones. It's partial because nothing is said about non-terminating executions.
A more recent idea was to flip this correctness logic to get an incorrectness logic, which says if you can reach a "bad" state (this is useful for bug detection.) In such a logic, you only want to know about reachable states, so the formula gets flipped: if the final program state satisfies the postcondition, then there must be a program state satisfying the precondition that can execute the program and terminate in that final state.
The difference between these two logics is one axis of this cube. There are other possible logics: you can ask if a precondition is necessary - that is, is the postcondition only reachable from states satisfying the precondition? It turns out there are two orthogonal approaches to stating such a property, and they form the other two axes of the cube.
That's a shockingly good Socratic dialog that maps fairly well! I've not read your dialog in detail; nor have I read this blog article enough times to know if the mapping is correct. However, a quick glance shows that it's in the same ballpark!
ivanbakel|1 year ago
A more recent idea was to flip this correctness logic to get an incorrectness logic, which says if you can reach a "bad" state (this is useful for bug detection.) In such a logic, you only want to know about reachable states, so the formula gets flipped: if the final program state satisfies the postcondition, then there must be a program state satisfying the precondition that can execute the program and terminate in that final state.
The difference between these two logics is one axis of this cube. There are other possible logics: you can ask if a precondition is necessary - that is, is the postcondition only reachable from states satisfying the precondition? It turns out there are two orthogonal approaches to stating such a property, and they form the other two axes of the cube.
aaronsnoswell|1 year ago
[deleted]
thechao|1 year ago
dev-jayson|1 year ago
aaronsnoswell|1 year ago