Example: Semantics: Program analysis: p1us卜（1，z2)→z1十2 p1us卜ZZ>{z1+z2|(z1,2)∈ZZ} where z1,z2∈Z where ZZC Z x Z Correctness relations Representation functions result Rz 3z(z)={z} argument RzxZ 8z×z(21,2)={(z1,2)} (plus上·→) plus (Rz×z→Rz） (8z×zBz)(p1us卜··) (plus卜·>·) E(plus卜·>·) PPA Section 4.1 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 16
Example: Semantics: plus ` (z1, z2) ❀ z1 + z2 where z1, z2 ∈ Z Program analysis: plus ` ZZ ✄ {z1 + z2 | (z1, z2) ∈ ZZ } where ZZ ⊆ Z × Z Correctness relations Representation functions result RZ βZ(z) = {z} argument RZ×Z βZ×Z(z1, z2) = {(z1, z2)} plus (plus ` · ❀ ·) (RZ×Z →→ RZ) (plus ` · ✄ ·) (βZ×Z →→ βZ)(plus ` · ❀ ·) v (plus ` · ✄ ·) PPA Section 4.1 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 16
Approximation of Fixed Points ●Fixed points 。Videning ●Narrowing Example:lattice of intervals for Array Bound Analysis PPA Section 4.2 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 17
Approximation of Fixed Points • Fixed points • Widening • Narrowing Example: lattice of intervals for Array Bound Analysis PPA Section 4.2 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 17
The complete lattice Interval =(Interval, [00,0∞]● -oo,1]0 [-1,oo] [-o0,0] [2,2 [0.oo [00,-1● -2,1]度-1,20 。[1,oo] 2,0] 1,1 [0,20 [2,-1] [1,0 [0,10 [1,2 -2,-2]●1，-1 [0,0p [1,1 2,2 PPA Section 4.2 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 18
The complete lattice Interval = (Interval, v) • ❩❩❩❩❩❩❩❩✚✚ ✚ ✚ ✚ ✚ ✚ ❛❛❛ ✚ • ❛❛❛❛❛❛❛❛❛❛❛❛❛✦✦✦✦✦✦✦✦✦✦✦✦✦✦✦✦ • ❅ ❅ ❅ ❅ • ❅ ❅ ❅ ❅ • ❅ ❅ ❅ ❅ ❅• ❅ ❅ ❅ • • ❅ ❅ ❅ ❅ • ❅ ❅ ❅ ❅ ❅• ❅ ❅ ❅ • • ❅ ❅ ❅ ❅ ❅• ❅ ❅ ❅ • ❅• ❅ ❅ ❅ • • • •❅ ❅ ❅ • ❅ •❅ ❅ ❅ [-∞,-1] • ❅• [-∞,0] [-∞,1] [-∞,∞] [-2,-2] [-2,-1] [-2,0] [-2,1] [-2,2] [-1,-1] [-1,0] [-1,1] [-1,2] [-1,∞] [0,0] [0,1] [0,2] [0,∞] [1,1] [1,2] [1,∞] [2,2] ⊥ PPA Section 4.2 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 18
Fixed points Let f:L-L be a monotone function on a complete lattice L=(L,E,U,几，⊥，T) l is a fixed point iff f(1)=l Fix(f)=f()= f is reductive at l iff f() Red(f)=f() f is extensive at l iff f() EXt(f)={l|f()彐 Tarski's Theorem ensures that Ifp(f)=Fix(f)=Red(f)E Fix(f)C Red(f) gfp(f)=Fix(f)=Ext(f)E Fix(f)C Ext(f) PPA Section 4.2 F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 19
Fixed points Let f : L → L be a monotone function on a complete lattice L = (L, v, t, u, ⊥, >). l is a fixed point iff f(l) = l Fix(f) = {l | f(l) = l} f is reductive at l iff f(l) v l Red(f) = {l | f(l) v l} f is extensive at l iff f(l) w l Ext(f) = {l | f(l) w l} Tarski’s Theorem ensures that lfp(f) = Fix(f) = Red(f) ∈ Fix(f) ⊆ Red(f) gfp(f) = F Fix(f) = F Ext(f) ∈ Fix(f) ⊆ Ext(f) PPA Section 4.2 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 19
Fixed points of f T ● fr(T) Red(f)------ ● 冂nfm(T) gfp(f) Fix(f)----- Ifp(f) Unfm(⊥) Ext(f)---- fm(⊥) ⊥ PPA Section 4.2 C F.Nielson H.Riis Nielson C.Hankin (Dec.2004) 20
Fixed points of f • • • • • • • • ⊥ f n(⊥) F n f n(⊥) lfp(f) gfp(f) nf n(>) f n(>) > Ext(f) Fix(f) Red(f) ✲ ✲ ✲ PPA Section 4.2 c F.Nielson & H.Riis Nielson & C.Hankin (Dec. 2004) 20