1. No, we can draw the dependency graph as follows

2. Yes, because the head \(p\) depends on the query \(r\) and vv. again as a graph we can draw it as follows

Let's consider a basic instance of abstraction where we think of the concrete domain as set's of numbers and the abstract domain as rangers or intervals of numbers which characterize these sets. So formally we say

• Our concrete domain is the power set \(\mathcal P(\mathbb {R})\) of the natural real numbers \(\mathbb {R}\) ordered by set-inclusion so \(\sqsubseteq \equiv \subseteq \)
• Our abstract domain is represented by intervals in addition to the symbols for true and false, so \[ A = \textrm {Intervals} \cup \{\top , \bot \} \]
• Our concretization function maps from an interval to all those numbers contained within the interval, so as an example \[ \gamma ([l, u]) \equiv \{x \mid l \leq x \leq u\} \]
• Our abstraction function which takes a concrete element \(c\) then maps this to the meet or conjunct of all abstract element in which the ordering with the concretization function holds, i.e. \[ \alpha (c) = \bigwedge \{a \in A \mid c \subseteq \gamma (a)\} \] the idea is that it represents the most precise abstract representation which can capture the concrete element c. Operationally we can express this equivalently as \[ \alpha(c \equiv \{x_1, x_2, \ldots, x_n\}) = \begin{cases} [\textrm{min}\ c, \textrm{max}\ c] & \textrm{if bounded} \\ [\textrm{min}\ c, +\infty) & \textrm{if only lb} \\ (-\infty, \textrm{max}\ c] & \textrm{if only ub} \\ \top & \textrm{if unbounded} \\ \bot & \textrm{if}\ = \emptyset \end{cases} \] so more plainly we can understand the abstraction function of just being the most exact combination i.e. meet / conjunction of intervals to express our concrete element.

A common application within the domain of logic and computer science is to consider the concrete domain as referring to formulas or equivalently set's of states, not too much unlike our power-set of numbers. With our abstract state then being a conjunct of predicates from some finite set \(P\) which best characterize our concrete formulas.

• Each element in the abstract domain is some permutation of our finite predicate set \(P\), so we have \[ A = \mathcal P(P) \quad P_1 \sqsubseteq P_2 \iff P_2 \subseteq P_1 \] each abstract element \(a \in P\) is defined by the conjunction \[ \bigwedge _{p \in a} p \] hence our concretization function yields those set's of concrete states (or predicates representing these states) which satisfy \(a\). \[ \gamma (a) = \{\sigma \in \Sigma \mid \forall p \in a.\ p(\sigma ) = \top \} \equiv \llbracket \bigwedge _{p \in a} p \rrbracket \]
• The abstraction function is then defined more or less the usual way, we take in a concrete set of states \(c\) then aggregate those predicates which describe our concrete set of states most precisely. \[ \alpha (c) = \bigcap \{a \in A \mid c \subseteq \gamma (a)\} \] can equivalent formulation is \[ \alpha (c) = \bigwedge \{p \in P \mid c \to p\} \]

Let's consider as an example

Here we can define the abstraction function as follows

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.