The Hoare Cube

I wrote earlier this year about my attempt to understand the repercussions of toggling and when giving a semantics to Hoare triples. In response to that post, Yann Herklotz helpfully pointed me to Patrick Cousot’s POPL 2024 paper [10], which does all this and a lot more besides. In particular, Cousot’s paper includes the following diagram…

…which shows how to obtain dozens of program logics just by toggling a handful of switches in the semantics.

However, that diagram is completely terrifying, and (just between you and me) I can’t get my head around much of the rest of Cousot’s paper. So, this blog post is my attempt to end up with a similar diagram to Cousot’s one, but while trying to keep things as simple as possible.

Let us assume that we have a set of states, and that a command is simply a binary relation on states. We shall write to mean that if command is started in state it can produce final state . Our commands need not always terminate: if there is no such that , then that means does not terminate when started in state . Also, our commands can be non-deterministic: if and with , then that means behaves non-deterministically when started in state .

The original “partial correctness” interpretation [1] of the Hoare triple is that whenever is started in a state satisfying the assertion (an assertion is just a set of states), any final state it reaches must satisfy the assertion . That is…

.

Let us define a helper function: the “strongest postcondition”. We shall write for the set of all states that command can reach if it starts executing in a state…

.

We can use to give a semantics to Hoare triples in a variety of different ways. For instance, the partial correctness interpretation given above can be rewritten as…

.

Flipping the into a to get Incorrectness logic…

…is what led O’Hearn to remark that “program correctness and incorrectness are two sides of the same coin”. But there are other components that can be “flipped” too. I think there are three “dimensions” in total:

(NB: Cousot seems to identify four dimensions in his diagram above, but I haven’t understood what his fourth one is.)

The eight options, then, are as follows:

Name(s)	Meaning of	Reach Direction Approximation
Partial correctness [1]		may forward over
Reverse Hoare logic [5], Incorrectness logic [6]		may forward under
Necessary preconditions (as formulated in [4])		may backward over
Backward under-approximate Hoare triple [2], Lisbon triple [3], Sufficient incorrectness logic [4], Possible correctness [9]		may backward under
Necessary preconditions (as originally formulated in [7])		must forward over
		must forward under
Partial correctness (alternative formulation)		must backward over
		must backward under

Note that partial correctness can also be rewritten into the more familiar if we define as the “weakest liberal precondition” in the usual way…

…but I quite like how “systematic” the table above is: it distinguishes may from must by negating the pre and postconditions; it distinguishes forward from backward by using or ; and it distinguishes over from under approximate by using or .

Note also that I’ve labelled as the “original” formulation of necessary preconditions, as it captures the two negatives in Cousot et al.’s definition quite nicely: “under which precondition, if violated, will the program always be incorrect?” [7, my emphasis].

We can assemble all eight options in the table into a cube — a “Hoare cube”, if you will.

In the cube, I’ve drawn solid lines between vertices that represent equal semantics. For instance, may+forward+over is equal to must+backward+over because…

.

Sometimes these equalities can be phrased as Galois connections. For instance…

…signifies a Galois connection between and .

I’ve also drawn dashed lines between vertices that represent equivalent semantics. By “equivalent” here, I mean that there exists a bijection between triples such that the triple holds according to one semantics if and only if the triple holds according to the other semantics. What this means is that one strategy for proving under one semantics is to prove under the other semantics.

For instance, may+backward+over (necessary preconditions, ) is equivalent to may+forward+over (partial correctness, ) because…

…as Ascari et al. have observed [4, Proposition 5.4]. Here we use the bijection that maps to .

For another instance, may+forward+under (incorrectness logic, ) is equivalent to may+backward+under (sufficient incorrectness logic, ) because, using another bijection that maps to , we have…

.

For this reason, I’ve deemed all of the over nodes equivalent (and coloured them green) and all of the under nodes equivalent (and coloured them blue).

But is it a bit of a stretch to consider all those same-coloured nodes “equivalent”? I mean, if the point of these bijections is to suggest how a proof in one logic can be transformed into a proof in another logic, then are these transformations reasonable? The bijection , for instance, requires the ability to invert an arbitrary command (turning into ). That’s straightforward enough for simple programs, thanks to properties like and and , but it could become infeasible in more complicated settings. Likewise, the bijection requires the ability to negate an arbitrary assertion (turning into ), which is fine in ordinary predicate logic but doesn’t work very nicely in a substructural logic like separation logic.

Still, it does give a pretty handy way to generate proof rules for one logic from the proof rules for another logic. For instance, Ascari et al. [4] present this proof rule from incorrectness logic…

…and if we apply our bijection to all the triples in this rule, then we obtain “for free” the corresponding proof rule from their sufficient incorrectness logic…

…without having to prove anything about its soundness.

To conclude: perhaps program correctness and incorrectness are not simply two sides of the same coin, but two opposite faces of the same cube!

Related work

Möller et al. [2, Section 5] define and briefly study “backward under-approximate Hoare triples”. Zilberstein et al. [3] refer to those triples also as “Lisbon triples”. Ascari et al. [4] define sufficient incorrectness logic as a proof system for those “backward under-approximate Hoare triples”, and I’m grateful to Ike Mulder who referred me to Ascari et al.’s paper in a comment on my earlier blog post.

Zilberstein et al. [3] defines and studies “Outcome logic”, but I haven’t included it in my “cube” because I don’t think it quite fits with the other logics – its postconditions are not simply “sets of states”, but have a more complicated monoidal structure. I also haven’t included “Exact separation logic” [11], which unifies over-approximate and under-approximate reasoning in the context of separation logic.

Zhang and Benjamin Kaminsky [8, Section 6.3] also studied the eight options in my table above, similarly obtained by toggling three binary switches (albeit with slightly different names), and I’m grateful to Benjamin for pointing me to his work in a comment on my earlier blog post. I’ve reproduced their table here:

The two blue rows in their table are equal, and they correspond to the two “partial correctness” vertices in my cube. The two orange lines are also equal, and they correspond to the two “necessary preconditions” vertices in my cube. I also haven’t got names for the ??? and ¿¿¿ logics, but I note that ??? can be straightforwardly obtained from sufficient incorrectness logic via the bijection I defined above, and ¿¿¿ can be obtained from incorrectness logic in the same way, so I think this makes it unlikely that those logics will offer anything particularly new.

For the record: one potential point of confusion in Zhang and Kaminsky’s table is that what they call “wp” is actually what O’Hearn [6, Section 6.3] calls the “weakest possible precondition”: the sets of states from which can reach a final state satisfying the postcondition (but due to non-determinism, might not). Thus, I think “total correctness” should probably be read as “possible correctness”, following Hoare’s terminology [9, Section 5.3].

Bibliography

• [1] C.A.R. Hoare: An axiomatic basis for computer programming. CACM, 1969.
• [2] Bernhard Möller, Peter O’Hearn, and Tony Hoare: On Algebra of Program Correctness and Incorrectness. RAMiCS, 2021.
• [3] Noam Zilberstein, Derek Dreyer, and Alexandra Silva: Outcome Logic: A Unifying Foundation for Correctness and Incorrectness Reasoning. OOPSLA, 2023.
• [4] Flavio Ascari, Roberto Bruni, Roberta Gori, and Francesco Logozzo: Sufficient Incorrectness Logic: SIL and Separation SIL. ArXiv, 2023.
• [5] Edsko de Vries and Vasileios Koutavas: Reverse Hoare Logic. SEFM, 2011.
• [6] Peter O’Hearn: Incorrectness Logic. POPL, 2020.
• [7] Patrick Cousot, Radhia Cousot, Manuel Fähndrich, Francesco Logozzo: Automatic Inference of Necessary Preconditions. VMCAI, 2013.
• [8] Linpeng Zhang and Benjamin Lucien Kaminsky: Quantitative Strongest Post. OOPSLA, 2022.
• [9] C.A.R. Hoare: Some properties of predicate transformers. JACM, 1978.
• [10] Patrick Cousot: Calculational Design of [In]Correctness Transformational Program Logics by Abstract Interpretation. POPL, 2024.
• [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. ECOOP, 2023.