« Mathematical foundations:
(5) Fixpoint theory »
Part I
Patrick Cousot
Jerome C. Hunsaker Visiting Professor
Massachusetts Institute of Technology
Department of Aeronautics and Astronautics
Fixpoints
cousot mit edu
www.mit.edu/~cousot
Course 16.399: “Abstract interpretation”
http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 1 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 3 —
ľ P. Cousot, 2005
Fixpoint
– A fixpoint of an operator f on a set L is x 2 L such
that f(x) = x
– An operator may have 0, 1 or many fixpoints (e.g.
–x . x)
Alfred Tarski
Reference
[1] A. Tarski. “A lattice-theoretical fixpoint theorem and its applications”. Pacific J. of Math., 5:285–310, 1955.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 2 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 4 —
ľ P. Cousot, 2005
Fixpoints, prefixpoint and postfixpoints
of an operator on a poset
Let f 2 L 7! L be an operator on a poset hL; vi. We define its
def
– set of fixpoints: fp(f ) = fx 2 L j f (x) = xg
def
– set of pre-fixpoints: prefp(f ) = fx 2 L j x v f (x)g
def
– dual set of post-fixpoints: postfp(f ) = fx 2 L j x w f (x)g
– Note that fp(f ) „ prefp(f ), fp(f ) „ postfp(f ) by reflexivity and
fp(f ) = prefp(f ) \ postfp(f ) by antisymmetry
– In general, these sets can be empty:
a and b not comparable for =
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 5 —
ľ P. Cousot, 2005
Notations for extreme (least/greatest)
fixpoints
– lfp (f) least fixpoint (if any)
- f(lfp f) = lfp f
- 8x 2 L : (f(x) = x) =) (lfp f v x)
– gfp f greatest fixpoint (if any)
- f(gfp f) = gfp f
- 8x 2 L : (f(x) = x) =) (gfp f w x)
If the order v is not clear from the context, we write
v
v
lfp f and gfp f to make it explicit.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 7 —
ľ P. Cousot, 2005
— 8 —
ľ P. Cousot, 2005
Extreme (least/greatest) fixpoints
A fixpoint x of an operator f 2 L 7! L on a poset hL; vi
is:
– The least fixpoint of f iff 8y 2 L : (f(y) = y) =)
(x v y)
– Dually, the greatest fixpoint of f iff 8y 2 L : (f(y) =
y) =) (x w y)
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 6 —
ľ P. Cousot, 2005
Iterates
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
Iterates of an operator on a set
Iterates of an operator on a finite set
– Let f be an operator on a set L. The iterates of f
from a 2 L are:
– Let hf n(a); n 2 Ni be the iterates 1 of f 2 L 7! L
– If L is finite of cardinality jLj < @0, we have 8k > jLj :
9n » jLj : f k (a) = f n(a) and so
- either the iterates reach a fixpoint:
f 0(a) = a
f n+1(a) = f(f n(a)) n 2 N
so that f n = f| ‹ f ‹{z: : : ‹ f}. We have (by recurrence):
n times
- or they reach a cycle:
f n+1 = f n ‹ f
f n ‹ f m = f n+m
(f n)m = f nˆm
1 also called “orbit”.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 9 —
ľ P. Cousot, 2005
Computation of the iterates
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 11 —
ľ P. Cousot, 2005
Basin of attraction
– All iterates ending in the same cycle are called a basin
of attraction
– Since
f 2n = (f n)2
f 2n+1 = f ‹ (f n)2
we can compute f n in time O(ln n) provided f n can
be computed in the same time as f (which is often not
the case except in few cases like functions represented
by polynomials or BDDs which can be composed symbollically before doing the computation)
– The relation x ” y () 9i; j 2 N : f i(x) = f j (y) is
an equivalence 2. Each class contains exactly one cycle
(including the particular case of fixpoints). And so the
set L is partitionned into disjoint basins of attraction.
2 For transitivity, if f i (x) = f j (y) and f k (y) = f ‘ (z) and e.g. j » k then f i+d = f j+d = f k (y) = f ‘ (z) where
d=j`k –0
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 10 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 12 —
ľ P. Cousot, 2005
Iterates of an operator on an infinite set
If L is infinite of cardinality jLj – @0, we have three
possibilities
– either the iterates reach a fixpoint:
Fixpoint example 1:
Numerical fixpoint
– or they reach a cycle:
– or the iteration is infinite:
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 13 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 15 —
ľ P. Cousot, 2005
– Example of iterates converging to a fixpoint cos x = x
Fixpoint Examples
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 14 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 16 —
ľ P. Cousot, 2005
Fixpoint example 2:
Equivalence relation
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 17 —
Fixpoint example 3:
Grammar semantics
ľ P. Cousot, 2005
Example of fixpoint definition: equivalence relations
Let S be a set. We have the complete lattice of relations h}(S ˆ S); „; ;; S ˆ S; [; \i. Given r „ S ˆ S,
let f(r) = –x . 1S [ r [ x`1 [ x ‹ x. f(r) is monotonic.
„
Its least fixpoint lfp; f(r) is the least equivalence reladef
„
tion including r. The map E = –r . lfp; f(r) is an upper
closure operator which fixpoints are exactly the equivalence relations on S ˆ S, which by Ward’s theorem is
therefore a complete lattice hE(}(S ˆ S)); „; 1S ; S ˆ S;
–X . E([X) 3; \i.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 19 —
ľ P. Cousot, 2005
Example of fixpoint definition:
semantics of context free grammars
The meta syntax of grammars is:
T
N
"
G ::= P j P G
P ::= N ‘::=’ R
R ::= T R j N R j "
Terminals T 2 T
Nonterminals N 2 N
Empty
Grammar
Production/rule P 2 P
righthand side
3 The union of equivalence relations need not be an equivalence relation, but the transitive closure of a union
of equivalence relations is an equivalence relation, indeed the least.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 18 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 20 —
ľ P. Cousot, 2005
Example of meta derivation
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 21 —
The above equations have exactly the same least fixpoint as:
‘(X) = ‘(Y ) ´ ‘(X) [ ‘(Y ) [ ‘(X)
‘(Y ) = fag [ fbg [ ‘(Y )
The equations can be rewritten as:
‘ = ‘[X := ‘(Y ) ´ ‘(X)] [_ ‘[X := ‘(Y )] [_ ‘[X := ‘(X)]
[_ ‘[Y := fag] [_ ‘[Y := fbg] [_ ‘[Y := ‘(Y )]
that is
‘ = F (‘)
where
F (‘) = ‘[X := ‘(Y ) ´ ‘(X)] [_ ‘[X := ‘(Y )] [_ ‘[X := ‘(X)]
[_ ‘[Y := fag] [_ ‘[Y := fbg] [_ ‘[Y := ‘(Y )]
The operator F = SJGK associated to a grammar G can be defined by structural induction on the metagrammar.
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 23 —
ľ P. Cousot, 2005
Example of grammar semantics
Structural definition of the grammar semantics
Let ‘(X) be the language generated by the nonterminal
X in grammar G. The Rice-Ginsburgh/Schützenberger
equations:
Given a grammar G = hT ; N ; A; Pi with axiom A 2 N ,
m
define SJGK 2 (N 7! T ~˜) 7`! (N 7! T ~˜) by
‘(X) = ‘(Y ) ´ ‘(X) [ ‘(Y )
‘(Y ) = fag [ fbg
SJN ‘::=’ RK‘ = ‘[N := SJRK‘]
SJP GK‘ = SJP K‘ [_ SJGK‘
SJT RK‘ = fT g ´ SJRK‘
(where the concatenation of languages is X ´ Y = fffff 0 j
ff 2 X ^ff 0 2 Yg) have a least fixpoint which associate the
language generated by the grammar to each nonterminal
‘ = fX ! (ajb)+; Y ! ajbg.
SJN RK‘ = ‘(N ) ´ SJRK‘
SJ"K = f~›g
_
„
The semantics of G is (lfp _ SJGK)(A)
;
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 22 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 24 —
ľ P. Cousot, 2005
Example
G = X ::= Y X
SJX ::= Y X
X ‘::=’ Y
X ‘::=’ Y
Y ‘::=’ a Y ‘::=’ b
Y ‘::=’ a
= SJX ::= Y XK‘ [_ SJX ‘::=’ Y
Iterative resolution of the equations
Y ‘::=’ bK‘
Y ‘::=’ a
Y ‘::=’ bK‘
= SJX ::= Y XK‘ [_ SJX ‘::=’ Y K‘ [_ SJY ‘::=’ a
Y ‘::=’ bK‘
= SJX ::= Y XK‘ [_ SJX ‘::=’ Y K‘ [_ SJY ‘::=’ aK‘ [_ SJY ‘::=’ bK‘
= ‘[X := SJY XK‘] [_ ‘[X := SJY K‘] [_ ‘[Y := SJaK‘] [_ ‘[Y := SJbK‘]
= ‘[X := SJY XK‘ [_ SJY K‘] [_ ‘[Y := SJaK‘ [_ SJbK‘]
= ‘[X := ‘(Y ) ´ SJXK‘ [_ SJY K‘] [_ ‘[Y := SJaK‘ [_ SJbK‘]
= ‘[X := ‘(Y ) ´ ‘(X) ´ SJ"K‘ [_ ‘(Y ) ´ SJ"K‘] [_ ‘[Y := fag ´ SJ"K‘ [_ fbg ´ SJ"K‘]
= ‘[X := ‘(Y ) ´ ‘(X) ´ f~›g [_ ‘(Y ) ´ f~›g] [_ ‘[Y := fag ´ f~›g [_ fbg ´ f~›g]
= ‘[X := ‘(Y ) ´ ‘(X) [ ‘(Y )] [ ‘[Y := fag [_ fbg]
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 25 —
ľ P. Cousot, 2005
so that the equation
‘ = SJGK‘
is
8
< ‘(X) = ‘(Y ) ´ ‘(X) [ ‘(Y ) [ ‘(X)
‘(Y ) = fag [ fbg [ ‘(Y )
:
‘(Z) = ‘(Z)
when Z 62 fX; Y g
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 26 —
ľ P. Cousot, 2005
–
–
–
–
–
–
–
8
< X = Y ´ X [ Y) [ X
Y = fag [ fbg [ Y
:
Z = Z
when Z 62 fX; Y g
X 0 = Y0 = Z0 = ;
X 1 = ;, Y 1 = fa; bg, Z 1 = ;
X 2 = fa; bg, Y 2 = fa; bg, Z 2 = ;
S
X 3 = fa; bg ´ fa; bg [ fa; bg [ fa; bg = faa; ab; ba; bb; a; bg = 2i=1(ajb)i
...
Sn`1
X n = i=1
(ajb)i
induction hypothesis
n+1
n
X
=S
X ´ Yn [ Yn [ X n
Sn`1
n`1
= i=1
(ajb)i ´ (ajb)1 [ (ajb)1 [ i=1
(ajb)i
Sn`1
S
n`1
i+1
i
= i=1 (ajb) [ i=1 (ajb)
S
S
i
= nj=2(ajb)j [ n`1
j =i+1
i=1 (ajb)
Sn
j
= j=1(ajb)
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 27 —
ľ P. Cousot, 2005
– ...
S
S
Sn`1
S
Sn`1
S
– X ! = n<! X n = 2»n<! i=1
(ajb)i n<! i=1
(ajb)i = n–1(ajb)n = (ajb)+
– X !+1 = X ! ´ Y ! [ Y ! [ X !
= (ajb)+ ´ (ajb) [ (ajb) [ (ajb)+ = (ajb)+ = X !
_
_
„
„
so lfp _ SJGK = fX ! (ajb)+; Y ! (Ajb)g whence for the axiom lfp _ SJGK(X)
;
;
= (ajb)+.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 28 —
ľ P. Cousot, 2005
m
_ g 2 L 7`m! L then mon(f) v
_
– We conclude that mon(f) 2 L 7`! L and if f v
g.
t
u
m
Theorem. The set L 7`! L of monotone maps on a
complete lattice hL; v; ?; >; t; ui is a complete lattice
m
_ >;
_ t;
_ ?;
_ ui
_
hL 7`! L; v;
Fixpoint example 4:
Lattice of closure operators
m
Proof. Observe that mon is an upper closure operator and L 7`! L =
m
_ >;
_ –S . mon(tS);
_ mon(?);
_
mon(L 7! L). By Ward theorem, hL 7`! L; v;
_ is a complete lattice. By duality, we can define
ui
l
def
mon0 = –f . –x . ff(y) j y w xg
m
so that mon0 is a lower closure operator and L 7`! L = mon0(L 7! L). By the
m
_ mon0(>);
_ t;
_ ?;
_ –S . mon(uS)i
_
dual of Ward theorem, hL 7`! L; v;
is a complete
_ =?
_ and –S . mon(uS)
_
lattice. Combining the two results, we get mon(?)
= u_
m
_ >;
_ t;
_ ?;
_ ui.
_
whence the complete lattice hL 7`! L; v;
t
u
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 29 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 31 —
ľ P. Cousot, 2005
The complete lattice of monotone operators
on a complete lattice
The complete lattice of extensive operators
on a complete lattice
Let hL; v; ?; >; t; ui be aG
complete lattice and define
def
mon = –f . –x . ff(y) j y v xg
Theorem. Let hL; v; ?; >; t; ui be a complete lattice.
def
Define ext = –f . –x . x t f(x). Then ext(f) is the least
extensive operator greater than of equal to f 2 L 7! L.
ext is an upper closure operator. The set hext(L 7! L);
_ t;
_ –x . x; >;
_ ui
_ is the complete latttice of extensive
v;
operators on L.
Lemma. Given f 2 L 7! L, mon(f) is the least monotone
operator v-greater than of equal to f
Proof. – Given a; b 2 L such that a v b, we have y v b implies a v y so
ff(y) j y v ag „ ff(y) j y v bg proving mon(f)a „ mon(f)b so mon(f) is
monotone.
_ mon(f).
– Observe that x „ x so f(x) 2 ff(y) j y v xg proving that f v
m
_
– Let g 2 L 7`! L be such that
F f v g. We have
F 8y 2 L : f(y) vFg(y) so
that 8a 2 L : mon(f)(a) = ff(y) j y v ag v fg(y) j y v ag v fg(y) j
_ g
g(y) v g(a)g v g(a) proving that mon(f) v
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 30 —
ľ P. Cousot, 2005
Proof. – An operator f on L is extensive iff ext(f) = f.
_ g and g is extensive then ext(f) = –x . x t f(x) v
_ –x . x t g(x) = g.
– If f v
_ >;
_ –S . ext(tS);
_ ext(?);
_
_ is a complete lattice by
– So hext(L 7! L); v;
ui
Ward’s theorem.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 32 —
ľ P. Cousot, 2005
_ = –x . x and if S „ ext(L 7! L) is a set of extensive opeartors
– But ext(?)
F
F
F
on L then 8x 2 L : x v f(x) so x v f2S f(x) = ( _ S)(x) proving _ S to
F
F
_
be extensive so –S . ext(tS)
= –S . _ S = _ .
t
u
– We have uclo(f)(x) = lfp (–y . xtmon(f)(y)) so uclo(f)(x) = xtmon(f)(uclo(f)(x)))
w x, proving uclo(f) to be extensive.
– We have x v uclo(f)(x) so mon(f)(x) v mon(f)(uclo(f)(x)) by monotony.
Hence mon(f)(x) v uclo(f)(x) since uclo(f)(x) = lfp (–y . x t mon(f)(y)).
For idempotency, uclo(f)(uclo(f)(x)) = lfp (–y . uclo(f)(x)tmon(f)(y)).
The iterates are
y0 = ?
y 1 = uclo(f)(x) t mon(f)(?))
2
= uclo(f)(x) Hsince uclo(f)(x) w mon(f)(x) w mon(f)(?), by monotoony.I
y = uclo(f)(x) t mon(f)(uclo(f)(x)))
= uclo(f)(x) t uclo(f)(x)
= uclo(f)(x)
which is the limit of the iteration sequence.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 33 —
Fixpoint definition of the closure operators
on a complete lattice
Theorem. Let hL; v; ?; >; t; ui be a complete lattice.
Define
def
uclo = –f . –x . lfp (–y . x t mon(f)(y))
Then uclo(f) is the least upper closure operator greater
than of equal to f 2 L 7! L.
Proof. – Given f 2 L 7! L, mon(f) is monotone and so is –y . x t mon(f)(y)
so that by Knaster-Tarski fixpoint theorem (on page 39), lfp (–y . xtmon(f)(y))
exists for all x 2 L and so uclo is well defined.
– If x1 v x2 then –y . x1 t mon(f)(y) v –y . x2 t mon(f)(y) so that, by the
fispoint comparison theorem (on page 73), we have uclo(f)(x1) = lfp (–y . x1 t
mon(f)(y)) v lfp (–y . x2 t mon(f)(y)) = uclo(f)(x2) proving uclo(f) to be
monotonic.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 34 —
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
ľ P. Cousot, 2005
ľ P. Cousot, 2005
Hsince uclo(f)(x) is monotonicI
— 35 —
ľ P. Cousot, 2005
_ mon(f) v
_ f so that uclo(f) is pointwise greater
– We have proved uclo(f) v
than of equal to f.
_ g then –y . xtmon(f)(y) v
_ –y . xtmon(g)(y) so lfp (–y . xtmon(f)(y))
– If f v
_
.
v lfp (–y x t mon(f)(y)) by forthcoming fixpoint comparison theorem (on
_ uclo(g) whence that uclo is monotonic
page 73) proving that uclo(f) v
– Let  be a closure operator. We have uclo()(x) = lfp (–y . x t mon()(y)) =
lfp (–y . x t (y) since  is monotone. Let us compute the transfinite iterates
y0 =
1
y =
v
y‹ v
?
x t (?)
(x)
Hsince ? v x so (?) v (x) by monotony and x t (?) v
(x) t (?) = (x)I
(x)
Hinduction hyppthesisI
y ‹+1 = x t (y ‹ )
v x t ((x))
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
Hby monotonyI
— 36 —
ľ P. Cousot, 2005
= x t (x)
Hby idempotencyI
= (x)
Hby extensivityI
F
˛
–
If – is a limit ordinal and 8˛ < – : y v (x) then y = ˛<– y ˛ v (x).
By transfinite induction all iterates are upper bounded by (x) whence so
is the least fixpoint lfp (–y . x t mon(f)(y)) which is one of these transfinite
iterates (by forthcoming constructive fixpoint theorem. We conclude that
uclo(f)(x) v (x).
_ 
– Finally, given a closure operator  greater that or equal to f, we have f v
_
which implies by monotony uclo(f) v uclo() =  so that uclo(f) is the least
upper closure operator greater than or equal to f.
t
u
Corollary. The set uclo(L 7! L) of upper closure operator on a complete lattice hL; v; ?; >; t; ui is a complete
_ –S . uclo(tS);
_
_
lattice huclo(L 7! L); v; –x . x; >;
ui
t
u
Proof. By Ward’s theorem.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 37 —
ľ P. Cousot, 2005
— 38 —
Theorem. A monotonic map ’ 2 L 7! L on a complete lattice:
hL; v; ?; >; t; ui
has a least fixpoint:
lfp ’ = u postfp(’);
(1)
= ufx 2 L j ’(x) v xg
and, dually, a greatest fixpoint:
(2)
gfp ’ = t prefp ’;
= tfx 2 L j x v ’(x)g
Reference
[2] A. Tarski. A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics,
5:285–310, 1955.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 39 —
ľ P. Cousot, 2005
Proof. – Let a = uP and P = postfp(’) = fx 2 L j ’(x) v xg.
– For all x 2 P , we have:
- avx
[a glb of P ]
- ’(a) v ’(x)
[’ monotonic]
- ’(a) v x
[def. P and transitivity]
whence ’(a) is a lower bound of P .
– ’(a) v a
[’(a) lower bound of P and a glb of P ]
=) ’(’(a)) v ’(a)
[’ monotonic]
=) ’(a) 2 P
[def. P ]
=) a v ’(a)
[a lower bound of P ]
=) ’(a) = a
[antisymmetry]
– If ’(x) = x then x 2 P whence a v x since a is the greatest lower bound
of P .
– gfp ’ = t prefp ’ by duality (replacing v; ?; >; t; u respectively by w; >; ?; u; t
in the above proof).
t
u
Fixpoint theorems
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
Knaster-Tarski fixpoint theorem for monotone
operators on a complete lattice
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 40 —
ľ P. Cousot, 2005
Theorem. The set of fixpoints of a monotone operator
m
f 2 L 7`! L on a complete lattice hL; v; ?; >; t; ui is
a complete lattice.
Proof. – We know that fp(f) is not empty.
– Let X „ fp(f)
F
- The interval L0 = [ X; >] is a complete lattice
- Let a = lfp fjL0 be the least fixpoint of f restricted to L0
- We have
1. a 2 fp(f)
F
2. 8x 2 X : x v tX v a since X is the infimum of L0
F
3. if y 2 fp(f) is such that 8x 2 X : x v y, we have X v y so y 2 L0
proving that a v y
– The fixpoint can be unique:
but in general there are many.
– In general, the set of fixpoints is not a sublattice of L.
A counter example is
a and b are fixpoints
of f but c = a t b is
not.
Reference
[3] A. Tarski. A lattice theoretical fixpoint theorem and its applications. Pacific Journal of Mathematics,
5:285–310, 1955.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 41 —
ľ P. Cousot, 2005
– It follows that a is the lub of X „ fp(f) in fp(f) for v proving that hfp(f); vi
is a complete lattice.
t
u
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 43 —
ľ P. Cousot, 2005
Reflexive/strict transitive closure of a binary
relation on a set (remainder from lecture 4)
Let S be a set and r; r1; r2 „ S ˆ S be relations on S:
def
– r1 ‹ r2 = fhx; zi j 9y : x r1 y ^ y r2 zg composition
def
– 1S = fhx; xi j x 2 Sg
def
– r 0 = 1S
identity
powers
def
– r n+1 = r n ‹ r (= r ‹ r n)
def S
– r ? = n2N r n
def S
– r + = n2Nnf0g r n
reflexive transitive closure
strict transitive closure
so r ? = r + [ 1S
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 42 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 44 —
ľ P. Cousot, 2005
Least fixpoint definition of the reflexive/strict
transitive closure
Theorem.
Least fixpoint definition of the lefthand side
restriction of the reflexive/strict transitive closure
Let S be a set, r „ S ˆ S be a relation on S, and E; F „
S. We define
„
r ? = lfp –X . 1S [ X ‹ r
„
r + = lfp –X . r ‹ (1S [ X)
def
left restriction
def
right restriction
E ‰ r = fhx; yi 2 r j x 2 Eg
r — F = fhx; yi 2 r j y 2 F g
Proof. – h}(S ˆ S); „; ;; S; [; \i is a complete lattice
We have
Theorem.
– –X . 1S [ X ‹ r is monotone since
=) X ‹ r „ Y
‹
r
=) 1S [ X r „ 1S [ Y
‹
„
E ‰ r ? = lfp –X . E ‰ 1S [ X ‹ r
X „Y
„
‹
r ? — F = lfp –X . 1S — F [ X ‹ r
r
– –X . r ‹ (1S [ X) is monotone since
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 45 —
ľ P. Cousot, 2005
— 47 —
ľ P. Cousot, 2005
Proof.
X „Y
=) (1S [ X) „ (1S [ Y )
=) r ‹ (1S [ X) „ r ‹ (1S [ Y )
– The existence of the fixpoints follows from Knaster-Tarski theorem
S
S
S
S
– We have r? = n2N rn = r0 [ n>0 rn = r0 [ n–0 rn+1 = r0 [ n–0 (r ‹ rn)
S
= r0 [ r ‹ ( n–0 rn) = 1S [ r ‹ r? so that r? is a fixpoint of –X . 1S [ X.
Let R be another fixpoint that is R = 1S [ X ‹ R. We have r0 = 1S „=
1S [ X ‹ R = R. Assume by induction hypothesis that rn „ R then
rn+1 = r ‹ rnS„ r ‹ R „ 1S [ X ‹ R = R. By recurrence, 8n : rn „ R
proving r? = n2N rn „ R to be the least fixpoint.
– The proof is similar for r+
t
u
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 46 —
ľ P. Cousot, 2005
r? = –X . 1S [ X ‹ r
\
=)
r? =
fX j 1S [ X ‹ r „ Xg
Knaster-Tarski
\
?
=) E ‰ r = E ‰ fX j 1S [ X ‹ r „ Xg
\
=
fE ‰ X j 1S [ X ‹ r „ Xg
\
=
fE ‰ X j E ‰ (1S [ X ‹ r) „ E ‰ Xg
\
=
fE ‰ X j E ‰ 1S [ (E ‰ X) ‹ r „ E ‰ Xg
\
=
fY j (E ‰ 1S ) [ Y ‹ r „ Y g
by letting Y = (E ‰ X)
„
= lfp –X . E ‰ 1S [ X ‹ r
The proof is similar for r? — F .
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
Knaster-Tarski
t
u
— 48 —
ľ P. Cousot, 2005
Banach’s lemma
David Park upper fixpoint induction principle 4
Theorem. Let A and B be two sets and suppose there exist
m
Theorem. Let f 2 L 7`! L on hL; v; ?; >; t; ui.
two maps f 2 A 7! B and g 2 B 7! A. Then there exist
partitions A = A1 [ A2 with A1 \ A2 = ; and B = B1 [ B2 with
B1 \ B2 = ; such that f (A1) = B1 and g(B2) = A2.
Proof. h}(A); „; ;; A; [; \i is a complete lattice. Define F (X) = A n
g(B n f(X)). If X „ Y then f(X) = ff(x) j x 2 Xg „ ff(x) j x 2 Y g =
f(Y ) so (B n f(X)) « (B n f(Y )) so g(B n f(X)) « g(B n f(Y )) whence
(A n g(B n f(X))) „ (A n g(B n f(X))), that is F (X) „ F (Y ), proving F
„
to be monotone. By Knaster-Tarski, we can define A1 = lfp; F . Moreover
define A2 = A n A1, B1 = f(A1 ) and B2 = B n B1 so that we have partitions.
It remains to prove that g(B2) = A2. Indeed A n g(B2) = A n g(B n B1) =
A n g(B n f(A1 )) = F (A1) = A1 by the fixpoint property. It follows that g(B2)
= A n (A n g(B2)) = A n A1 = A2 Q.E.D.
t
u
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 49 —
ľ P. Cousot, 2005
v
lfp f v P
() 9I 2 L : f(I) v I ^ I v P
Proof. (() Soundness
If f(I) v I then I 2 fX 2 L j F (X) v Xg so by Knaster-Tarski
d
v
lfp f = fX 2 L j F (X) v Xg v I, whence by I v P and transitivity,
v
lfp f v P
()) Relative completenesss
v
v
Assume lfp f v P . Choose I = lfp f. Then f(I) v I by reflexivity
and I v P by hypothesis and def. I.
t
u
4 This induction principle is very important and underlies many safety proof methods (such as Floyd/Naur
for partial correctness). By analogy, I is called an invariant.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
The Cantor-Schröder-Bertein theorem
Proof. We apply Banach’s lemma and by injectivity jA1j = jB1j and jA2j =
jB2j so jAj = jBj.
t
u
ľ P. Cousot, 2005
Application to the relational forward
deductive positive proof principle
Corollary. Let A and B be two sets and suppose there exist
injective maps f 2 A  B and g 2 B  A. Then there exists a
bijective map h 2 A 
“ B of X onto Y .
— 51 —
Theorem.
8s; s 2 S : (s 2 E ^ hs; si 2 t? ^ s 2 F ) =) hs; si 2 ¯
, 9I : 8s; s0; s : s 2 E =) hs; si 2 I
^ (hs; s0i 2 I ^ hs0; s00i 2 t) =) hs; s00i 2 I
^ (hs; si 2 I ^ s 2 F ) =) hs; si 2 ¯
Proof.
8s; s 2 S : (s 2 E ^ hs; si 2 t? ^ s 2 F ) =) hs; si 2 ¯
() 8s; s 2 S : (hs 2 E ^ s; si 2 t?) =) (s 2 F =) hs; si 2 ¯ )
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 50 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 52 —
ľ P. Cousot, 2005
() E ‰ t? „ P
Hwhere P = fhs; si 2 S 2 j (s 2 F ) =) (hs; si 2 ¯ )gI
„
() (lfp –X . E ‰ 1S [ X ‹ t) „ P
() 9I 2 L : (E ‰ 1S [ I ‹ t) v I ^ I v P
A variant of the Knaster-Tarski fixpoint
theorem for monotone operators on a poset
m
() 9I 2 L : E ‰ 1S v I ^ I ‹ t v I ^ I v P
() 9I 2 L : 8s; s 2 S : [s 2 E ^ s = s =) hs; si 2 I] ^ [9s0 : hs; s0i 2
I ^ hs0; si 2 t =) hs; si 2 I] ^ [hs; si 2 I =) hs; si 2 P ]
() 9I : 8s; s0; s : [s 2 E =) hs; si 2 I] ^ [(hs; s0i 2 I ^ hs0; si 2 t) =)
hs; si 2 I] ^ [(hs; si 2 I ^ s 2 F ) =) hs; si 2 ¯ ]
t
u
Theorem. Let f 2 L 7`! L be a monotone operator on
a poset hL; vi which possesses a least postfixpoint p:
f(p) v p ^ 8x 2 L : (f(x) v x) =) (p v x)
then
v
v
lfp f = p ^ 8x 2 L : (f(x) v x) =) (lfp f v x)
Proof. – Since p postfp(f) and f is monotone, we hace f(f(p)) v f(p) so p v
f(p) since p is the least postfixpoint of f, we get f(p) = p by antisymmetry.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 53 —
ľ P. Cousot, 2005
David Park lower fixpoint induction principle
m
Theorem. Let f 2 L 7`! L on hL; v; ?; >; t; ui.
— 55 —
ľ P. Cousot, 2005
– Let x be any fixpoint of f. f(x) = x implies f(x) v x by reflexivity so
v
p v x proving that p = lfp f.
t
u
Example:
v
P v gfp f
() 9I 2 L : I v f(I) ^ P v I
t
u
Proof. By duality.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 54 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 56 —
ľ P. Cousot, 2005
Least fixpoint of a monotone operator greater
than or equal to a given prefixpoint
v
We write lfpa f for the v-least fixpoint of f 2 L 7! L
on the poset hL; vi greater than or equal to a (if it ever
exists):
v
Taking a = ?, we get the Knaster-Tarski classical result.
v
Observe that if a 6v f(a) then lfpa f may not exist, as
shown by the following counter-example:
v
– a v lfpa f = f(lfpa f)
v
– 8x 2 L : [a v x = f(x)] =) [lfpa f v x]
m
Theorem. If f 2 L 7`! L on hL; v; ?; >; t; ui and
v
a 2 prefp(f) then lfpa f exists.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 57 —
def
ľ P. Cousot, 2005
m
Proof. – L0 = [a; >] v L is a complete lattice and f 2 L0 7`! L0 since
x 2 L0 =) a v x =) f(a) v f(x) =) a v f(x) since a v f(a). By
v
Knaster-Tarki lfp fjL0 exists on L0 and is a fixpoint of f 2 L 7! L greater
than or equal to a
– It is the least since any other one x would have a v x = f(x) = fjL0 (x)
would not be the least one of fjL0 on L0.
t
u
— 59 —
ľ P. Cousot, 2005
David Park upper fixpoint induction principle
revisited
m
Theorem. If f 2 L 7`! L on hL; v; ?; >; t; ui and
a 2 prefp(f), P 2 L then
v
m
Corollary. If f 2 L 7`! L on hL; v; ?; >; t; ui and
d
v
a 2 prefp(f) then lfpa f = fx 2 L j a v x ^ f(x) v xg.
v
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
v
Proof. By Knaster-Tarski, lfpa f = lfp fjL0 =
d
fx 2 L j a v x ^ f(x) v xg.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
d
fx 2 L0 j fjL0 (x) v xg =
t
u
— 58 —
ľ P. Cousot, 2005
lfpa f v P
() 9I 2 L : a v I ^ F (I) v I ^ I v P:
Proof. by Park upper fixpoint induction principle on L0 = [a; >].
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 60 —
t
u
ľ P. Cousot, 2005
By duality,
m
Theorem. If f 2 L 7`! L on hL; v; ?; >; t; ui and
a 2 postfp(f), P 2 L then the greatest fixpoint of f less
than or equal to a exists and is
l
v
gfpa f =
fx 2 L j x v f(x) ^ x v ag
v
P v gfpa f () 9I 2 L : P v I ^ I v F (I) ^ I v a
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 61 —
ľ P. Cousot, 2005
Characterization of the least fixpoint of a
monotone operator greater than or equal to
a given prefixpoint 5
m
Theorem. If f 2 L 7`! L on hL; v; ?; >; t; ui and
v
v
a 2 prefp(f) then lfpa f = lfp? –x . a t f(x).
v
v
Proof. Let A = lfpa f and B = lfp? –x . a t f(x)
1. A = f(A) and a v A so a t f(A) v A t A = A proving that A 2
postfp(–x . a t f(x)) whence B v A by Knaster-Tarski.
2. We have B = a t f(B) whence a v B so f(a) v f(B). By hypothesis
a v f(a) so that by transitivity, a v f(B). It follows that a t f(B) =
f(B) whence B = f(B) and a v B so A v B, and by antisymmetry,
we get A = B.
t
u
5 Observe that we get the variant of Park induction principle on page 60 by applying the classical principle
of page 51 to B.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 62 —
ľ P. Cousot, 2005
Conjugate of an operator
on a complete boolean lattice (reminder)
– Let f 2 L 7! L be an operator on the complete boolean
lattice hL; v; ?; >; t; u; :i. We define
def
fe = –x . :f(:x)
to be the conjuguate of f in L.
– fe is sometimes denoted f ? (which may be confusing
with the reflexive transitive closure notation)
– fe is sometimes called the dual of f (which is confusing
with the lattice dual, but is consistent since x v y
() :x v :x).
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
m
— 63 —
ľ P. Cousot, 2005
–f . fe
_ ``
_
``
``
``
`
` hL 7`m! L; wi
– we have hL 7`! L; vi
!
Proof.
–f . fe
_ h
–f . fe(g) v
_
() ge v h
_ h(x)
() 8x 2 L : :g(:x) v
_ :h(x)
() 8x 2 L : g(:x) v
_ :h(x)
() 8x 2 L : g(:x) v
_ :h(:y)
() 8y 2 L : g(y) v
_ e
() g v
h
_
() g v –f . fe(h)
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
Hby letting y = :xI
t
u
— 64 —
ľ P. Cousot, 2005
Park unique fixpoint condition
in a complete boolean lattice
Park conjugate (dual) fixpoint theorem in
complete boolean lattices
m
m
Theorem. Let f 2 L 7`! L be a monotone operator
on the complete boolean lattice hL; v; ?; >; t; u; :i.
Then
gfp f = :lfp –x . :f(:x)
lfp f
= :gfp –x . :f(:x)
Theorem. Let f 2 L 7`! L be a monotone operator
on the complete boolean lattice hL; v; ?; >; t; u; :i.
Then
(1) lfp –x . :f(:x) u lfp f = ?
(2) (lfp –x . :f(:x) t lfp f = >) () (lfp f = gfp f)
Proof. If x v y then :y v :x so f(:y) v f(:x) whence :f(:x) v :f(:y)
m
proving –x . :f(:x) 2 L 7`! L whence by Knaster-Tarski that the extreme
fixpoints do exist.
Proof.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 65 —
=
=
=
=
= gfp f
HKnaster-TarskiI
HComplete bool. latticeI
:gfp f v :lfp f
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
=)
:gfp f u :lfp f v :lfp f u lfp f
=)
:gfp f u :lfp f v ?
=)
:gfp f u :lfp f = ?
=)
lfp –x . :f(:x) u lfp f = ?
— 67 —
ľ P. Cousot, 2005
HComplete bool. latticeI
Hby letting y = :xI
HKnaster-TarskiI
By duality lfp f = :gfp –x . :f(:x).
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
lfp f v gfp f
ľ P. Cousot, 2005
We have
:lfp –x . :f(:x)
l
: fx j :f(:x) v xg
G
f:x j :f(:x) v xg
G
f:x j :x v f(:x)g
G
fy j y v f(y)g
(1)
=)
t
u
— 66 —
ľ P. Cousot, 2005
(2, () lfp –x . :f(:x) = :gfp f so lfp f = gfp f implies > = :lfp f t lfp f =
:gfp f t lfp f = lfp –x . :f(:x) t lfp f = >
(2, )) By (1) and the hypothesis lfp –x . :f(:x)tlfp f = >, we get lfp –x . :f(:x)
and lfp f are complement hence :(lfp –x . :f(:x)) = lfp f proving that is
lfp f = gfp f by the previous theorem due to Park.
t
u
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 68 —
ľ P. Cousot, 2005
Application to the relational forward
predictive contrapositive proof principle
Theorem.
8s; s 2 S : (s 2 E ^ hs; si 2 t? ^ s 2 F ) =) hs; si 2 ¯
, 9I : 8s; s : (s 2 E ^ hs; si 62 ¯ ) =) hs; si 2 I
^ hs; si 2 I =) [8s0 2 S : hs; s0i 2 t =) hs0; si 2 I]
^ s 2 F =) hs; si 62 I
Proof.
Theorem. Let hL; vi and hM; »i be complete lattices
m
m
and f 2 L 7`! M , g 2 M 7`! L. Then g(lfp f ‹ g) =
lfp g ‹ f.
Proof. – (g ‹ f)(g(lfp f ‹ g) = g(f ‹ g(lfp f ‹ g)) = g(lfpdf ‹ g) so g(lfp f ‹ g) 2
fx j g ‹ f(x) v xg so, by Knaster-Tarski, lfp g ‹ f = fx j g ‹ f(x) v xg v
g(lfp f ‹ g).
– Let x 2 L be such that g ‹ f(x) v x.
() 8s; s 2 S : (s 2 E ^ hs; si 2 t? ^ s 2 F ) =) hs; si 2 ¯
?
() 8s; s 2 S : (hs; si 2 t ^ s 2 F ) =) (s 2 E =) hs; si 2 ¯ )
?
Fixpoint of the composition of
monotone functions
=) f(g ‹ f(x)) » f(x)
2
() t — F „ fhs; si 2 S j (s 2 E) =) (hs; si 2 ¯ )g
=) f
() t? — F „ P
=) lfp f
HP = fhs; si 2 S 2 j (s 2 E) =) (hs; si 2 ¯ )gI
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 69 —
ľ P. Cousot, 2005
‹
g(f(x)) » f(x)
‹
‹
g) v g ‹ f(x)
() :gfp –X . :(t ‹ (:X) [ 1S — F ) „ P
=) g(lfp f
‹
g) v x
() 9I : :P „ I ^ I „ :(t ‹ (:I)) ^ (1S — F ) „ :I
() 9I : 8s; s : (s 2 E ^ hs; si 62 ¯ ) =) hs; si 2 I ^ hs; si 2 I =) :[9s0 2
S : hs; s0i 2 t ^ hs0; si 62 I] ^ s 2 F =) hs; si 62 I
() 9I : 8s; s : (s 2 E ^ hs; si 62 ¯ ) =) hs; si 2 I ^ hs; si 2 I =) [8s0 2 S :
hs; s0i 2 t =) hs0; si 2 I] ^ s 2 F =) hs; si 62 I
t
u
HKnaster-TarskiI
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
=) g(lfp f
() 9I : :P „ I ^ I „ :(t ‹ (:I)) ^ I „ :(1S — F )
Hby def. ‹I
g » f(x)
() lfp –X . t ‹ X [ 1S — F „ P
() :P „ gfp –X . :(t ‹ (:X)) \ :(1S — F )
Hby monotonyI
— 71 —
ľ P. Cousot, 2005
Hby monotonyI
Hby hyp. g ‹ f(x) v x and transitivity I
d
So g(lfp f ‹ g) v fx j g ‹ f(x) v xg = lfp g
Tarski
– By antisymmetry, g(lfp f ‹ g) = lfp g ‹ f.
‹
f by def. glb and Knaster-
t
u
Other equivalent induction principles are found in [4].
Reference
[4] P. Cousot and R. Cousot. Induction principles for proving invariance properties of programs. In Tools
& Notions for Program Construction: an Advanced Course, D. Néel (Ed.), Cambridge University Press,
Cambridge, UK, pp. 75–119, August 1982.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 70 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 72 —
ľ P. Cousot, 2005
Fixpoints of pointwise comparable monotone
operators on a complete lattice
m
Theorem. Let f; g 2 L 7`! L be a pointwise comparable monotone operators on the complete boolean lattice
_ g. Then lfp f v lfp g.
hL; v; ?; >; t; u; :i: f v
d
_
Proof.
d f v g implies fx j f(x) v xg „ fx j g(x) v xg whence fx j g(x) v
xg v fx j f(x) v xg by def. of lubs whence lfp f v lfp g by Knaster-Tarski.
t
u
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 73 —
ľ P. Cousot, 2005
Abstraction soundness
Corollary.
lfp f v P
m
_ g ^ lfp g v P
() 9g 2 L 7`! L : f v
The soundness of static analysis or abstract model checking directly results from this principle since concrete verification conditions for f are replaced by mode abstract
verification conditions for g with which the proof is performed.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 74 —
ľ P. Cousot, 2005
The Bekić–Leszczylowski fixpoint theorem
m
m
Theorem. Let F 2 Ln+m 7`! Ln and G 2 Ln+m 7`! Lm be
monotone operators and hL; v; ?; >; t; ui be a complete lattice.
We write hX; Y i = hX1; : : : ; xn; Y1; : : : ; Ymi when x 2 Ln and
Y 2 Lm. Let us consider the
 set of equations
X = F (X; Y )
(1)
Y = G(X; Y )
the resolvant R = –Y . lfp –X . F (X; Y ) and the system of equations:

X = R(Y )
(2)
Y = G(R(Y ); Y )
Let us write fp(I) and lfp (i), i = 1; 2 for the respective set of
fixpoints and least componentwise solution of (i). We have
fp(2) „ fp(1) and lfp (2) = lfp (1)
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 75 —
ľ P. Cousot, 2005
_ hX; Zi so –X . F (X; Y ) v
_
Proof. – If Y; Z 2 Lm then Y v Z implies hX; Y i v
_
_
.
.
.
–X F (X; Z) so lfp –X F (X; Y ) v –X F (X; Z) whence R(Y ) v R(Z)
m
proving that R 2 Lm 7`! Ln whence fp(2) is not empty.
– Let hA2B2; 2i fp(2) be a fixpoint of (2). Then A2 = R(B2) so lfp –X . F (X; B2) =
A2 whence A2 = F (A2; B2) and B2 = G(R(B2); B2) that is B2 = G(A2 ; B2)
proving that hA2B2; 2i fp(1) so fp(2) „ fp(1).
– In general fp(2) 6= fp(1). A counter-example is provided by L = f?; >g
with ? v ? v > v >,

F (X; Y ) = X u Y
G(X; Y ) = X t Y
so that the resolvant is R = –Y . lfp –X . F (X; Y ) = –Y . lfp –X . X u Y =
–Y . ?. The system of equation (1) has the solution h>; >i which is not a
solution of (2) in that particular case.
_ lfp (2).
– Since lfp (2) 2 fp(1) we have lfp (1) v
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 76 —
ľ P. Cousot, 2005
– Let hA1B1; 2i fp(1) be a fixpoint of (1). We have F (A1; B1) = A1 whence
_ A1 whence A1 is a pointfixpoint of –X . F (X; B1) which implies
F (A1; B1) v
_ A1 that is R(B1) v
_ A1. Since
by Knaster-Tarski that lfp –X . F (X; B1) v
_ hA1; B1i and G is monotone G(R(B1); B1) v
_ G(A1; B1) v
_
hR(B1); B1i v
B1 since hA1; B1i is a postfixpoint of (1). It follows that hA1; B1i is a
_ hA1 ; B1i in particular lfp (2) v
_
postfixpoint of (2) which implies lfp (2) v
lfp (1).
– By antisymmetry, lfp (1) = lfp (2).
t
u
=) lfp f u P = lfp f
Hdef. glbI
(b) lfp f v P
=) f(lfp f) v f(P )
HmonotonyI
=) lfp f v f(P )
HfixpointI
=) lfp f = lfp f u P
Hdef. glbI
(c) if lfp f v P then
f(lfp f u P )
v f(lfp f) u f(P )
Hmonotony and def. glbI
= lfp f u f(P )
HfixpointI
= lfp f
Hby (b)I
= lfp f u P
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
ľ P. Cousot, 2005
— 77 —
Fixpoint clipping
Hby (a)I
t
u
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 79 —
ľ P. Cousot, 2005
Fixpoint induction with clipping
m
m
Theorem. Let f 2 L 7`! L be a monotone operator on
the complete boolean lattice hL; v; ?; >; t; u; :i and
P 2 L. Then
Theorem. Let f 2 L 7`! L be a monotone operator on
the complete boolean lattice hL; v; ?; >; t; u; :i and
P 2 L. Then
lfp f v P () f(lfp f u P ) v (lfp f u P )
lfp f v P
() 9I 2 L : f(I) u P v I ^ f(I) v P
Proof.
(() f(lfp f u P ) v (lfp f u P )
=) lfp f v lfp f u P
=) lfp f = lfp f u P
=) lfp f v P
HKnaster-TarskiI
Hlfp f u P v lfp f and antisymetryI
Hdef. glbI
()) (a) lfp f v P
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 78 —
ľ P. Cousot, 2005
Proof.
()) Let I = lfp f. f(I) u P = f(lfp f) u P = lfp f u P = lfp f = I since lfp f v P .
Moreover, f(I) = f(lfp f) = lfp f v P proving that 9I 2 L : f(I) u P v
I ^ f(I) v P .
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 80 —
ľ P. Cousot, 2005
(() Reciprocally, f(I) v P so f(I) u P = f(I) which by f(I) u P v I implies
f(I) v I, proving lfp f v I by Knaster-tarski. Since f is monotone lfp f =
f(lfp f) v f(I) v P proving lfp f v P by transitivity.
t
u
So the proof consists in:
1. Finding an invariant I 6 with the semantics clipped
by absence of runtime errors:
– 8s 2 ˚JP K : (s 2 E ^ s 62 ˙JP K) =) hs; si 2 I
– 8s; s0; s 2 ˚JP K : (hs; s0i 2 I ^ hs0; si 2 t ^ s 62
˙JP K) =) (hs; si 2 I)
2. Checking the absence of runtime error:
– 8s 2 ˚JP K : s 2 E =) s 62 ˙JP K
– 8s; s0; s 2 ˚JP K : (hs; s0i 2 I ^ hs0; si 2 t) =)
(s 62 ˙JP K)
6 e.g. by automatic static analysis
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 81 —
ľ P. Cousot, 2005
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 83 —
ľ P. Cousot, 2005
Application to the proof of
absence of runtime errors
–
–
–
–
˚JP K: set of states of a program P
tJP K „ ˚JP K ˆ ˚JP K: small-step operational semantics
EJP K „ ˚JP K: initial states
˙JP K „ ˚JP K: erroneous state
THE END
The absence of run-time errors is 8s; s 2 ˚JP K:
s 2 E ^ hs; si 2 (tJP K)? =) s 62 ˙JP K
() EJP K ‰ (tJP K)? „ (1˚JP K — :˙JP K)
Hdef. „I
() lfp f „ S
Hby the fixpoint definition of the lefthand side
def
restriction of the reflexive transitive closure on page 47 and, where f =
def
–X . EJP K ‰ 1˚JP K [ X ‹ tJP K and S = 1˚JP K — :˙JP KI
() 9I 2 ˚JP K ˆ ˚JP K : f(I) \ S „ I ^ f(I) „ S
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 82 —
ľ P. Cousot, 2005
My MIT web site is http://www.mit.edu/~cousot/
The course web site is http://web.mit.edu/afs/athena.mit.edu/course/16/16.399/www/.
Course 16.399: “Abstract interpretation”, Tuesday April 5th, 2005
— 84 —
ľ P. Cousot, 2005