Over approximate or under

A subject the papers are about. The loosest grouping, and the one to reach for last.

One connective, used in four directions. A Hoare triple's postcondition over-approximates what a program can reach and so proves bad states absent; reverse the inclusion and the same shape proves them present. Which end is fixed, and which way the approximation runs, is what decides what a program logic can promise.

The four directions are the two binary choices crossed. *Forward and over*: Hoare's triple, where the postcondition contains everything reachable, so anything outside it cannot happen -- the shape that proves absence. *Backward and over*: Dijkstra's weakest precondition, which fixes the other end and asks what must hold beforehand. *Under*: de Vries and Koutavas's reverse Hoare logic and O'Hearn's incorrectness logic, where every state in the postcondition genuinely is reachable, so the triple proves a bug is there rather than that none is. Cousot's abstract interpretation is the general theory of the approximation itself, with the 2010 gentle introduction as the way in, and Iris is the modern framework built on the over-approximating side.

The set holds a documented priority, which is why both under-approximating records are here rather than just the famous one. De Vries and Koutavas published reverse Hoare logic at SEFM in 2011, nine years before incorrectness logic, and O'Hearn's paper says so in as many words -- 'I acknowledge the priority of de Vries and Koutavas' -- crediting Emanuele D'Osualdo for pointing the earlier work out to him. A reader who meets incorrectness logic first, as most will, should know the shape was published in 2011 and did not travel.

That pattern recurs across the corpus and is worth naming: Grassmann before Peano in `the-axioms-before-peano`, Karger and Schell before Thompson in `trust-you-did-not-create`, Turing before Floyd in `relatively-complete`. Here the corpus holds both records and the acknowledgement is in the later paper's own text.