The abstract strongest postcondition, denoted \(\texttt {sp}^\#\) or \(\textrm {post\#}\) is defined as
\[
\texttt {sp}^\# (s, a) = \alpha (\texttt {sp}(s, \gamma (a)))
\]
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:
\[
\texttt {sp}(s, \gamma (a)) \subseteq \gamma (\texttt {sp}^\#(s, a))
\]
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 \)
\[
\forall a \in A, c \in C.\ \alpha (c) \subseteq a \iff c \leq \gamma (a)
\]
which expresses the notion that \(c\) is approximated by \(a\). We can rewrite our earlier soundness condition as:
\[
\alpha (\texttt {sp}(s, \gamma (a))) \sqsubseteq \texttt {sp}^\# (s, a)
\]
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.
\[
\texttt {sp}^\# (s, a) = \alpha (\texttt {sp}(s, \gamma (a)))
\]