Analyses Based on Formulas

Many analyses can be viewed in this way.

Fixpoint Approach

Let the domain be the set of quantifier-free formulas of some logic, ordered by implication

Is this a partial order?

Non-existence of limits: infinite disjunction need not be a formula of our logic, e.g. consider formulas on linear arithmetic and take the limit In general, a logic that can represent exact least upper bounds needs to express the conditions such as “there exists a sequence of statements that produces the given state”.

Approximation

Rule for computing formula (called 'fact') in step at program point  where is some approximation function. This is analogous to Abstract interpretation recipe.

Here the goal of is to ensure termination (and efficiency). The essential condition is that is a valid formula.

One generic approch: use a syntactic widening.

View formula as a conjunction. Then define Why are there no infinite chains when using such ?

To make it less syntactic: deduce some consequences of the conjunction (taken from a finite set): where where is some class of useful formulas.

Constraint-Based Approach

Give up least fixpoint requirement (it is approximation anyway).

Search for any fixpoint - it will be a set of loop invariants: Works better if we also have postconditions and assertions that need to be satisfied (otherwise we may come up with trivial invariants).

Assume a 'template' for the invariant, e.g. (Karr's analysis) each fact is a linear equation on program variables .

The condition for loop invariants gives a system of equations on coefficients for each of the finitely many program points .

If there exists a solution, this gives an invariant.

X := 10
Y := 0
while (X >= 0) {
X := X-1
if random() { Y = Y+1 }
}

Invariant of the form .   Such equations need to hold for all values of , , which gives constraints on that can be solved based on properties of real fields (linear programming, Farkas lemma).

Thanks to quantifier elimination for real fields, the technique extends to polynomial invariants as well.

If there is no solution, there is no invariant of that particular template form.

Note: for non-numerical domains, we obtain different kinds of constraints. A popular class are set constraints.