Lecture 9 Skeleton
Static analysis as equation solving in a lattice
If instead of formulas as we have elements of some lattice, this condition becomes
(where sp in now denotes operator on states and not formulas).
By properties of Galois connection, this is equivalent to
and we defined best transformer as , so this condition is equivalent to
We conclude that finding an inductive invariant expressed using elements of a lattice corresponds to finding a solution to a system of inequations for all . We next examine the existence and computation of such solutions more generally.
Note that is a function monotonic in a. Why?
So, we are solving a conjunction of inequations
where are variables ranging over a lattice (one for each control-flow graph node), and are monotonic functions on (one for each edge in the control-flow graph).
From a system of equations to one equation
In lattice, we have that a conjunction of inequations
is equivalent to ( is least upper bound of them).
So we can write the conjunction of inequations in the previous section as a system of equations
Now, introduce a new product lattice with order iff ,\ldots, all hold. Then we have reduced the problem to finding a solution to equation
where . Function is also monotonic.
The solution of equation of the form is called a fixed point of function , because leaves in place.
The iterative process that we described above corresponds to picking an initial element such that and then computing , \ldots, .
- we have
- we have
If it stabilizes we have , so is a fixed point. This always happens if there are no infinite ascending chains.
What is we have arbitrary lattices? See, for example non-converging iteration in reals.
-continuity in a complete lattice is a requirement that for every chain we have
(generalizes continuity in real numbers). For continuous functions, even if there are infinite ascending chains, the fixed point iteration converges in the limit.
In general, even without -continuity we know that the fixed point exists, due to Tarski fixed point theorem.
See also lecture notes in SAV07 resource page, in particular notes by Michael Schwartzbach for the finite case and slides by David Schmidt for -continuity. You can also check papers by Cousot & Cousot: