Abstract Interpretation:
concrete and abstract semantics (ctd.)
Semantics of statements
We can extend the semantics of expressions considered
so far to statements, mapping concrete/abstract states to
concrete/abstract states.
m’x=e (i)(S) = S [x/me(i)]
m’S;S’ (i)(S) = m’S’(i) (m’S (i)(S))
m’if e=f then S else S’ (i)(S) = m’S(i) (S) if me(i) = m f(i)
= m’S(i) (S) otherwise
s’x=e (i)(D) = D [x/se(i)]
s’S;S’ (i)(D) = s’S’(i) (s’S (i)(D))
s’if e=f then S else S’ (i)(D) = lub( s’S(i) (D), s’S’(i) (D))
Concrete and abstract semantics: while
Observe that:
while b do S
is equivalento to:
if !b skip; else {S; while b do S}
The semantics of the while statement can be expressed
(both at the concrete and abstract level) as a fixpoint
operator
Concrete semantics: while
m’while e1=e2 do S (i)(S) = S
if me1(i) != me2(i)
= m’S; while e1=e2 do S(i)(S) otherwise
s’while e1=e2 do S (i)(D) = lub(D, s’S;while e1=e2 do S (i)(D) )
= lub(D, s’while e1=e2 do S(i) (s’S (i)(D))
= lub(D, lub(D, s’S;while e1=e2 do S (i) (s’S (i)(D)))
= lub(D, s’S;while e1=e2 do S (i) (s’S (i)(D)) = …
Recursion
• As a final step, we add recursive functions (on a single
paramether)
program 
def f (x )  e
e  ... | f (e )
• Until now, the concrete semantics was defined as:
m : Exp  Int  Int
5
Concrete semantics (function calls)
• In order to take into account the call of functions, the
signature of m becomes as folllows:
m  : Exp  (Int  Int )  Int  Int
mf (e ) ( g )( j )  g ( me ( g )( j ))
mx ( g )( j )
j
me e ( g )( j )  me ( g )( j )  me ( g )( j )
1
2
1
2
6
Semantics of recursive functions
m  : Exp  (Int  Int )  Int  Int
Consideriamo una funzione
def f  e
Definiamo una catena ascendente f0 ,f1 ,... in Int  Int
f0  x . 
fi 1  me (fi )
Definiamo mf 
i
fi
7
def f = if x=0 then 1 else f(x - 1)
f0(i) = 
for every i
f1(i) = m’if x=0 then 1 else f(x - 1)(f0)(i) =
m’1(f0)(i) = 1
if
m’f(x - 1)(f0)(i)
otherwise
i=0
= f0 (m’x - 1(f0)(i))
= f0 (m’x (f0)(i)
- m’1 (f0)(i))
= f0 (i -1)
=
8
def f = if x=0 then 1 else f(x - 1)
f0(i) =  for each i
f1(i) = 1
if
i=0,  otherwise
f2(i) = m’if x=0 then 1 else f(x - 1)(f1)(i) =
m’1(f1)(i)=1
if
m’f(x - 1)(f1)(i)
otherwise
i=0
= f1 (m’x - 1(f1)(i))
= f1 (m’x (f1)(i)
= f1 (i
- m’1 (f1)(i))
- 1) = 1 if i=0, and  otherwise
9
def f = if x=0 then 1 else f(x - 1)
f0(i) =  for every i
f1(i) = 1
if
i=0,  otherwise
f2(i) = 1
if
i=0,1,  otherwise
f3(i) = 1
if
i=0,1,2,  otherwise
f4(i) = 1
if
i=0,1,2,3,  otherwise
...
m(f) = Ui>=0 fi
10
Abstract Semantics
• Tn the same way, we need to extend the definition of the
abstract semantics s.
• We require that all the operations are monotone.
s  : Exp  (A  A)  A  A
s f (e ) ( g )(i )  g (s e ( g )(i ))
s x ( g )(i )
i
s e e ( g )(i )  s e ( g )(i )  s e ( g )(i )
1
2
1
2
11
Abstract semantics of recursion
s ': Exp  (A  A)  A  A
Consideriamo una funzione
def f  e
Definiamo una catena ascendente f 0 ,f 1 ,... in A  A
f 0  a . 
f i 1  s e (f i )
Definiamo s f 
i
fi
12
Correctness
f2 ( j )


f1 ( j )


f0 ( j )

f2 ( j )

f 1(j )

f 0(j )
• The abstract chain always covers the corresponding element in
the concrete chain
13
Correctness (ctd.)
i . fi ( j )   (f i ( j ))

i 0
fi ( j ) 
i 0
 (f i ( j ))
le catene convergono



fi ( j )    f i ( j )  monotonia di 
i 0
 i 0

 mf ( j )   (s f ( j ))
per definizione
14
def f = if x=0 then 1 else f(x - 1)
f0(a) = 
for every a in Sign
f1(a) = s’if x=0 then 1 else f(x - 1)(f0)(a) =
if a=0
s’1(f0)(a)= +
if a=T
lub(s’1(f0)(a), s’f(x - 1)(f0)(a)) =
lub( +, f0 (s’x - 1(f0)(a))) =
lub( +, ) = +
if a=+,-
s’f(x - 1)(f0)(a) =
f0 (s’x - 1(f0)(a)) =
f0 (s’x (f0)(a) - s’1(f0)(a)) =
f0 (a - +) = f0 (T) = 
15
def f = if x=0 then 1 else f(x - 1)
f0(a) = 
for every a in Sign
f1(a) = + for 0,T and  for +,-
f2(a) = s’if x=0 then 1 else f(x - 1)(f1)(a) =
if a=0
s’1(f1)(a)= +
if a=T
lub(s’1(f1)(a), s’f(x - 1)(f1)(a)) =
lub( +, f1 (s’x - 1(f0)(a))) =
lub( +, f1 (s’x (f1)(a) - s’1(f1)(a)) ) =
lub(+, f1 (T - +)) = lub(+, f1 (T)) = +
if a=+
s’f(x - 1)(f1)(a) = f1 (s’x - 1(f1)(a)) =
f1 (s’x (f1)(a) - s’1(f1)(a)) =
f1 (+ - +) = f1 (T) = 
16
if a=-
s’f(x - 1)(f1)(a) = f1 (s’x - 1(f1)(a)) =
f1 (s’x (f1)(a) - s’1(f1)(a)) =
f1 (- - +) = f1 (-) = 
def f = if x=0 then 1 else f(x - 1)
f0(a) = 
for every a in Sign
f1(a) = +
for 0,T and  for +,-
f2(a) = +
for 0, +,T and  for –
f3(a) = f2(a)
fixpoint
s(f) = Ui>=0 fi = f2(a)
18
Summary
• Abstract Interpretation means
–
–
–
–
–
Define a concrete (collecting) smenatics
Define an abstract semantics (domain and operations)
Prove the local correctness of the operations
Apply a fixpoint algorithm to compute the abstract semantics
Use a widening operator to ensure convergence (if the
ascending chain condition does not hold)
19