of abstract domains. Let us recall that the lattice of abstract domains $\tuple{\operatorname{Abs}(C),\sqsubseteq}$ is isomorphic to the lattice of ucos on $C$ $\tuple{\operatorname{uco}(C),\sqsubseteq}$, where $\sqsubseteq$ denotes the pointwise ordering between functions, so that lub’s and glb’s of abstractions can be equivalently characterized in $\operatorname{uco}(C)$. Let us also recall that each $\mu\in \operatorname{uco}(C)$ is uniquely determined by its image $\operatorname{img}(\mu)=\mu(C)$ because $\mu = \lambda
x. \wedge \!\{ y\in C~|~ y\in \mu(C), \, x\leq y\}$. Moreover, a subset $X\subseteq C$ is the image of some uco on $C$ iff $X$ is meet-closed, i.e. $X=\ok{\operatorname{Cl}_\wedge 
(X){\triangleq}}\{ \wedge Y~|~ Y\subseteq
X\}$ (note that $\top_C =\wedge \varnothing \in \operatorname{Cl}_\wedge (X)$). Often, we will identify ucos with their images. This does not give rise to ambiguity, since one can distinguish their use as functions or sets according to the context. Hence, if $A,B\in \operatorname{Abs}(C)$ are two abstractions then they can be viewed as images of two ucos on $C$, denoted respectively by $\mu_A$ and $\mu_B$, so that $A$ is more precise than $B$ when $\operatorname{img}(\mu_B) \subseteq \operatorname{img}(\mu_A)$.

Let $f:C{\rightarrow}C$ be some concrete semantic function — for simplicity, we consider 1-ary functions — and let $\ok{f^\sharp:A {\rightarrow}A}$ be a corresponding abstract function defined on some abstraction $A\in 