Sol 2

Prof. Dr. P. Thiemann, Dipl.-Math. A.
Bieniusa Summer term 2010
Lecture: Program analysis

Exercise 2
http://proglang.informatik.uni-freiburg.de/teaching/programanalysis/2010ss/
Exercise 1: Complete lattices

1. Let M = {a, b, c}. Define a relation R such that (M, R) is a complete lattice.
2. For a totally ordered set S, (P(S), ⊆) is a complete lattice. Define another relation R
such that (P(S), R) is a complete lattice.
3. Is (R, ≤) a complete lattice? If not, how can you extend R such that it becomes a complete
lattice?
4. Let | be the relation of divisibility, i.e. a | b means a divides b. Is
• (N, |)
• (N\{0}, |)
• (N\{0} ∪ {∞}, |)
a complete lattice?
Solution
1. Define a < b and b < c. Then (M, ≤) is a complete lattice where ≤ is the reflexive and
transitive hull of <.
2. An easy solution is (P(S), ⊇). Another relation can be constructed like this: Let < be a
total order on S. You can order all elements of a subset of S with <. Using this, you can
construct a monotonic sequence of the subset (Careful! This does not work in general!
For this to work, the subset must have a least element). If we take the lexicographical
order <l on these sequences, we get again a complete lattice for (P(S), <l ).
3. (R, ≤) is not a complete lattice. For example, tN does not exist. The extension (R ∪
{±∞}, ≤) with
∀x ∈ R : −∞ < x < +∞ (1)
is a complete lattice.
4. a | b is defined as ∃c : a · c = b.
• | is reflexive: ∀a ∃c : a · c = a. Choose c = 1.
• | is transitive: ∀a, b, c with ∃d : a · d = b and ∃d0 : b · d0 = c. Then ∃e : a · e = c.
Choose e = d · d0 .
• | is antisymmetric: ∀a, b with ∃c : a · c = b and ∃c0 : b · c0 = a ⇒ a · cc0 = a ⇒
cc0 = 1 ⇒ c = c0 = 1 ⇒ a = b.
Hence, (N, |) is a partially ordered set. Let M ⊆ N. We have to distinguish now two
cases:
• |M | ∈ N and 0 ∈/ M . Then, uM = gcd(M ) (greatest common divisor) and tM =

lcm(M ) (least common multiple).
• |M | = ∞ or 0 ∈ M . Then, uM = gcd(M \{0}) and tM = 0.
In particular, > = 0 and ⊥= 1. Hence, (N, |) is a complete lattice.

Because (N\{0}, |) has no greatest element, it is not a complete lattice.
(N\{0} ∪ {∞}, |) is again a complete lattice with > = ∞.
Exercise 2: Comparing different approaches
Consider the following WHILE program from the slides:
[y := x]1 ;
[z := 1]2 ;
while [y > 0]3 do
[z := z ∗ y]4 ;
[y := y − 1]5 ;
[y := 0]6
Let F : (P(Var × Lab))12 → (P(Var × Lab))12 be the function defined by the data flow
equations (cf. slides on p. 31 ff.). Further, let (α, γ) be the Galois connection for the Reaching
Definitions analysis (cf. slides on p. 69 ff.)
~ ◦ G ◦ ~γ v F , i.e. show that

1. Prove that α
α(Gj (γ(RD1 ), . . . , γ(RD12 ))) ⊆ Fj (RD1 , . . . , RD12 )
holds for all j. Here, f~ denotes the application of function f to all entries of a tuple or
vector.
~ ◦ G ◦ ~γ .
2. Check whether F = α
α ◦ G ◦ ~γ )n (∅) v F n (∅).
3. Prove by induction over n that (~
~ (Gn (∅)) v (~
4. Prove that α α ◦ G ◦ ~γ )n (∅). You may use that α
~ (∅) = ∅ and G v G ◦ ~γ ◦ α
~.
Definitions The signatures of the functions are:
F : (P(Var × Lab))12 −→ (P(Var × Lab))12

G: (P(Trace))12 −→ (P(Trace))12
α : P(Trace) −→ P(Var × Lab)
γ : P(Var × Lab) −→ P(Trace)
α and γ are defined as follows:
α(X) = {(x, SRD(tr)(x) | x ∈ DOM(tr) ∧ tr ∈ X)}

γ(Y ) = {tr | ∀x ∈ DOM(tr) : (x, SRD(tr)(x)) ∈ Y }
where SRD(tr)(x) returns the label where the variable x has been set last in trace tr. DOM(tr)
is the set of variables for which SRD is defined.
Solution
1. There are three types of equations that correspond to each other:
(a) RDexit (l) = RDentry (l) and CSexit (l) = CSentry (l), RDentry (l) = RDexit (l − 1) and
CSentry (l) = CSexit (l − 1).
For the tuples we get: RDl = RDl−1 and CSl = CSl−1 .
(b) RDexit (l) = (RDentry (l)\{(x, l) | l ∈ Lab}) ∪ {(x, l)} and
CSexit (l) = {tr : (x, l) | tr ∈ CSentry (l)}
(c) RDentry (l) = RDexit (l − 1) ∪ RDexit (m) and
CSentry (l) = CSexit (l − 1) ∪ CSexit (m)
(a) We show as an example for l = 3 with RDexit (3) = RDentry (3) and CSexit (3) =
CSentry (3) that the assumption holds. All other cases of the same form are shown
analogously.
α ◦ Gexit (3)(~γ (RD)) = α ◦ Gexit (3) ×12

i=1 {tr | ∀x ∈ DOM(tr) :

(x, SRD(tr)(x)) ∈ RDi }

= α {tr | ∀x ∈ DOM(tr) : (x, SRD(tr)(x)) ∈ RDentry (3)}
n
= (x, SRD(tr)(x)) | x ∈ DOM(tr) ∧
o
tr ∈ {tr | ∀x ∈ DOM(tr) : (x, SRD(tr)(x)) ∈ RDentry (3)}
⊆ RDentry (3) = Fexit (3)(RD)
(b) Cf. book

(c) similar as (a)
2. Since γ is strictly monotonic, and α and G are monotonic, α ◦ G ◦ γ is strictly monotonic.

Further, F has a fixed point and therefore cannot be strictly monotonic. Hence, it holds
that
~ ◦ G ◦ ~γ @ F
α
3. n = 0:
α ◦ G ◦ ~γ )0 (∅) v F 0 (∅) = ∅
(~
n − 1 → n:
α ◦ G ◦ ~γ )n (∅) = (~
(~ α ◦ G ◦ ~γ )n−1 (~
α ◦ G ◦ ~γ )(∅)
≤IH F n−1 (~
α ◦ G ◦ ~γ (∅))
≤ F n−1 (F (∅)) = F n (∅)
since F is monotone.
4. As α is monoton, we can deduce:
~ ◦ Gn (∅) v α
α ~ )n (∅)
~ ◦ (G ◦ ~γ ◦ α
α ◦ G ◦ ~γ )n ◦ α
= (~ ~ (∅)
n
α ◦ G ◦ ~γ ) (∅)
= (~

Sol 2

Uploaded by

Copyright:

Available Formats

Sol 2

Uploaded by

Document Information

Original Description:

Original Title

Copyright

Available Formats

Share this document

Share or Embed Document

Sharing Options

Did you find this document useful?

Is this content inappropriate?

Copyright:

Available Formats

Sol 2

Uploaded by

Copyright:

Available Formats

Prof. Dr. P. Thiemann, Dipl.-Math. A.

Bieniusa Summer term 2010

Lecture: Program analysis

Exercise 1: Complete lattices

4. Let | be the relation of divisibility, i.e. a | b means a divides b. Is

• |M | ∈ N and 0 ∈/ M . Then, uM = gcd(M ) (greatest common divisor) and tM =

In particular, > = 0 and ⊥= 1. Hence, (N, |) is a complete lattice.

~ ◦ G ◦ ~γ v F , i.e. show that

α(Gj (γ(RD1 ), . . . , γ(RD12 ))) ⊆ Fj (RD1 , . . . , RD12 )

Definitions The signatures of the functions are:

F : (P(Var × Lab))12 −→ (P(Var × Lab))12

α and γ are defined as follows:

α(X) = {(x, SRD(tr)(x) | x ∈ DOM(tr) ∧ tr ∈ X)}

α ◦ Gexit (3)(~γ (RD)) = α ◦ Gexit (3) ×12

(b) Cf. book

2. Since γ is strictly monotonic, and α and G are monotonic, α ◦ G ◦ γ is strictly monotonic.

4. As α is monoton, we can deduce:

You might also like