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