In the previous article, we used value abstraction to prove that a simple opaque predicate always produces the same result. We introduced an abstract type parity_t and a function that takes a concrete uint32_t value and returns a parity_t:

1

parity_t parity_abstract(uint32_t x)

In the literature, this kind of abstraction function is usually denoted by a lowercase Greek letter alpha: α. So we can also write α(2) = even. An abstraction function has a corresponding concretization function (denoted by the Greek letter gamma: γ) that takes an abstract value and returns a set of concrete values. Why a set?

Our parity abstraction deliberately discards information: we retain only whether a value is even or odd. Thus, even may correspond to any even uint32_t value, odd to any odd one and unknown to any value whatsoever. Therefore, the output of the concretization function is necessarily a set:

1
2
3

γ(odd)  = {1, 3, 5, ... 4294967295}
γ(even) = {0, 2, 4, ... 4294967294}
γ(unknown) = {0, 1, 2, ... 4294967295}

Notice that γ(odd) and γ(even) are both subsets of γ(unknown). More formally:

1
2

γ(odd) ⊆ γ(unknown)
γ(even) ⊆ γ(unknown)

This brings us to an interesting property of our abstract domain. For any uint32_t value x:

1

{x} ⊆ γ(α(x)) 

Here, {x} is a singleton set containing x.

In other words, if we abstract a value x, then concretize the result, x will always be a member of this set.

Even though abstraction erases all the information about x except for its parity, the original value is always present in the concretized set. This property is called soundness and it is a necessary condition for a useful abstraction.

The soundness criterion also applies to the operations on abstract values (e.g. parity_sub and parity_mul). An implementation of parity_mul that always returned unknown would be sound but maximally imprecise. Conversely, an implementation that returned even for the product of two odd values would be unsound. Thus, even with a sound value abstraction, we must ensure that our abstract operations are sound and sufficiently precise for our purposes.

When working with abstract values, we can express the relationship between their concretizations using a precision ordering (⊑), read as being at least as precise as. Thus:

1
2

γ(odd) ⊆ γ(unknown) -> odd ⊑ unknown
γ(even) ⊆ γ(unknown) -> even ⊑ unknown

The two statements above mean that both odd and even are at least as precise as unknown. Indeed, α(2) = even describes the set of even integers up to UINT32_MAX; meanwhile unknown describes the set of all unsigned integers. Both contain our original 2, but unknown has twice as many possible values, introducing considerably more noise (i.e. values that aren't our original 2). And this is what makes even more precise: it contains less noise.

In the previous article we claimed that the parity abstraction we used was good, but we hand-waved the explanation of what makes it good. Now we can explain more precisely what makes it good. It is sound (as we showed above) and precise enough for the task at hand. As we established in the previous article: foo_abstract(EVEN) and foo_abstract(ODD) both produce EVEN.