O’Hearn’s Incorrectness Logic (IL) has recently gained a lot of traction in the programming languages community. While studying it with VT faculty and students, I became captivated by IL’s power of proving the presence of bugs. Before I delve into its practical application, I aim to gain a robust understanding of its precise meaning. Below, I’ve outlined some quick notes to grasp what IL is. In the future, I may write another post to explore how IL can be utilized.
Notation 1: We represent an IL triple as [P] C [Q], where P is considered a state predicate, or equivalently, a set of states satisfying such a state predicate.
Notation 2: The expression p ->C q denotes that executing C from state p could lead to state q if C terminates.
Definition: An IL triple [P] C [Q] is valid if, for any state q in Q, there exists a corresponding state p in P, such that p ->C q.
Examples:
- [P] C [False] is a valid IL triple for any P and C, because False represents an empty set of states.
- [x<=1] y = x + 1 [y<=2 /\ y = x + 1] is a valid IL triple since any state in Q, e.g., (x=0, y=1), can be reached from a state in P.
- [x<=1] y = x + 1 [y<=2] is not a valid IL triple because there exists a state in Q, (x=0, y=2), that cannot be reached from any state in P.
Hopefully, this basic understanding of IL will also serve a stepping stone for you to further investigate how this concept can be applied in various contexts.