Our usual strongest postcondition can be understood as a mapping from a concrete domain to a concrete domain, i.e.

Where \(C\) represents our concrete domain, in the world of program logic this is typically assertions on the state of some memory environment. The idea behind the abstract \(\texttt {sp}\), is that we have a function

In other words we are considering the strongest postcondition from within the abstract domain. Intuitively this just means that our predicates or assertions on the memory states (or equivalently the set of states we characterize) will be expressed in abstract terms.

The abstract strongest postcondition, denoted \(\texttt {sp}^\#\) or \(\textrm {post\#}\) is defined as

Let's explain a bit on how we can derive this, we begin with the idea that for each \(a \in A\) and each statement \(s\) we want:

This expresses soundness in other words, the resulting set of states, generated by concretizing the abstraction \(a\) must be contained within the prediction of the abstract transformer predicate \(\texttt {sp}^\#\). Then using the Galois connection we have between \(\alpha \) and \(\gamma \)

which expresses the notion that \(c\) is approximated by \(a\). We can rewrite our earlier soundness condition as:

two again denote the same conceptual thing that our abstract predicate transformer \(\texttt {sp}^\#\) is an over-approximation of the analogous transformer for the concrete domain. As we would preferably like to have the most precise approximation we choose equality. Or stated differently by definition the most precise abstracted approximation of the strongest post-condition we can have for some abstracted state is literally just this state concretized, and the resulting set abstracted.

The most important property to remember about the abstract strongest post-condition is that if we do over-approximate an error state it does not allow us to conclude that the program is wrong.