On Program Semantics

Transition Systems

The semantics of a program is defined classically in a very general way in small step operational form, as a transition system: , where is a set of states, is the subset of initial states, and is a transition relation. For sequential programs, the state set is defined as

where each state has a control part denoting the current program point, and a memory part mapping program variables to values . A transition models an atomic execution step, such as executing a machine-code instruction in a program. We denote by

the fact that , i.e., the program can reach the state from the state after one execution step. The transition system derives mechanically from the program code itself, e.g., from the sequence of binary instructions or, more conveniently, by induction on the syntax tree of the source code.

Example 1. Consider the simple programming language syntax:

where program points are denoted by and expressions by . The transition system is derived by induction on the syntax of as follows:

where denotes the function mapping to and every to , and states that expression evaluates to the value in memory .

Trace Semantics

We are not interested in the program itself, but in the properties of its executions. Formally, an execution trace is a finite sequence of states

such that and . The semantics we want to observe, which is called a collecting semantics, is thus defined in our case as the set of traces spawned by the program. It can be expressed as the least fixpoint of a continuous operator in the complete lattice of sets of traces:

That is, is the smallest set containing traces reduced to an initial state and closed under the extension of traces by an additional execution step. Note that we are observing partial execution traces; informally, we allow executions to be interrupted prematurely. Formally, is closed under prefix (it also includes the finite prefixes of non-terminating executions). This is sufficient if we are interested in safety properties, i.e., properties of the form “no bad state is ever encountered,” which is the case here — more general trace semantics, able to also reason about liveness properties.

A classic result is that can be restated as the limit of an iteration sequence:

It becomes clear then that computing is equivalent to testing the program on all possible executions (albeit with an unusual exhaustive breadth-first strategy), and that it is not adapted to the effective and efficient verification of programs: when the program has unbounded or infinite executions, is infinite.

(1) i := 2;                             at (1): i = 0 ∧ n = 0
(2) n := input int();                   at (2): i = 2 ∧ n = 0
(3) while i < n do                      at (3): 2 ≤ i ≤ max(2,n)
(4) if input bool() then i := i + 1;    at (4): 2 ≤ i ≤ n − 1 ∧ n ≥ 3
(5) done;                               at (5): 2 ≤ i ≤ n ∧ n ≥ 3
(6) assert i >= 2;                      at (6): i = max(2,n)

Example 2. The simple program increments in a loop, until it reaches a user-specified value .

Figure above presents its trace semantics starting in the state set . The program has infinite executions (e.g., if is never incremented).

State Semantics

We observe that, in order to prove safety properties, it is not necessary to compute exactly. It is sufficient to collect the set of program states encountered, abstracting away any information available in on the ordering of states. We use an abstraction function

defined as

An important result is that, as , the set can be computed directly as a fixpoint:

Equivalently, can be expressed as the iteration sequence

which naturally expresses that is the set of states reachable from after zero, one, or more transitions. The similarity in fixpoint characterisation of and is not a coincidence, but a general result of abstract interpretation (although, in most cases, the abstract fixpoint only over-approximates the concrete one: ).

Dually, given a set of states , one can construct the set of traces abstracted by using a concretization function

The pair forms a Galois connection. ¹

A classic result states that the best abstraction of can be defined as , which in our case turns out to be exactly . When the set of states is finite (e.g., when the memory is bounded), can always be computed by iteration in finite time, even if cannot. Obviously, may be extremely large and require many iterations to stabilize, hence computing exactly is not a practical solution; we will need further abstractions.

Program Proofs and Inductive Invariants

There is a deep connection between the state semantics and the program logic of Floyd–Hoare used to prove partial correctness. If we interpret each logic assertion at program point as the set of memory states satisfying it, and define

then the assertion family is a valid (i.e., inductive) invariant if and only if . Moreover, the best inductive invariant stems from , i.e., it is .

While, in proof methods, the inductive invariants must be devised by an oracle (the user), abstract interpretation opens the way to automatic invariant inference by providing a constructive view on invariants (through iteration) and allowing further abstractions.

Example 3. The optimal invariant assertions of the program in Fig. 1 appear in the right, and figure above presents graphically its state abstraction at point (3).

Memory Abstractions

In order to gain in efficiency on bounded state spaces and handle unbounded ones, we need to abstract further. As many errors (such as overflows and divisions by zero) are caused by invalid arguments of operators, a natural idea is to observe only the set of values each variable can take at each program point. Instead of concrete state sets in

we manipulate abstract states in

The concrete and abstract domains are linked through the following Galois connection (so-called Cartesian Galois connection):

Assuming that variables are integers or reals, a further abstraction consists in maintaining, for each variable, its bounds instead of all its possible values. We compose the connection with the element-wise lifting of the following connection between and intervals :

yielding the interval abstract domain.

Another example of memory domain is the linear inequality domain that abstracts sets of points in into convex, closed polyhedra. One abstracts by associating a polyhedron to each program point, which permits the inference of linear relations between variables. The polyhedra domain is thus a relational domain, unlike the domains deriving from the Cartesian abstraction (such as intervals).

Example 4.

Figure above presents the interval abstraction of the program in Fig. 1 at point (3). The relational information that when is lost.

Following the same method that derived the state semantics from the trace one, we can derive an interval semantics from the state one: it is expressed as a fixpoint of an interval abstraction of . While it is possible to define an optimal as — where combines and — this is a complex process when is large, and it must be performed for each , i.e., for each program. To construct a general analyzer, we use the fact that , and so , are built by combining operators for atomic language constructs, as in Example 1. It is thus possible to derive as a combination of a small fixed set of abstract operators. More precisely, we only have to design abstraction versions of assignments, tests, and set union. Generally, the combination of optimal operators is not optimal, and so the resulting is not optimal. Additionally, due to efficiency and practicality concerns, the base abstract operators may be chosen non-optimal to begin with. Achieving a sound analysis, i.e.,

only requires sound abstract operators, i.e., . The fact that , and even the existence of an function, while sometimes desirable, is by no means required — for instance, the polyhedra domain does not feature an abstraction function as some sets, such as discs, have no best polyhedral abstraction.

Example 5. The interval abstraction of a simple addition maps the interval environment

at point to

at point , which is optimal.

Example 6. The optimal abstraction would map to . However, the combination maps to instead, which is coarser when .

Example 7. We can design a sound non-optimal fall-back abstraction for arbitrary assignments by simply mapping to .

We now know how to define systematically a sound abstract operator which can be efficiently computed. Nevertheless, the computation of by naive iteration may not converge fast enough (or at all). Hence, abstract domains are generally equipped with a convergence acceleration binary operator , called widening. Widenings extrapolate between two successive iterates and ensure that any sequence

converges in finite time, possibly towards a coarse abstraction of the actual fixpoint.

Example 8. The classic interval widening sets unstable bounds to infinity:

When analyzing Fig.~1, the iterations with widening at (3) give the following intervals for : and , which is stable.

To balance the accumulation of imprecision caused by widenings and combining separately abstracted operators, it is often necessary to reason on an abstract domain strictly more expressive than the properties we want to prove — e.g., the polyhedra domain may be necessary to infer variable bounds that the interval domain cannot infer, although it can represent them, such as in Example 6.