CS550 Exam Solution

Do not open the exam until we tell you to. The exam is three hours long.
Place your CAMIPRO card on your desk.
Put all electronic devices in a bag away from bench.
Write using permanent, dark pen (no graphite nor heat-disappearing pen).
Write answers to different problems on disjoint sheets of paper that we supply.
Write your name, SCIPER and question number on the top-right of each sheet you return.
Do not write the solutions that you want us to grade on the sheets with exam questions; please take these printed exam sheets with you after the exam.
You are only allowed one, A4-sized, two-sided cheat sheet.
The maximal number of points on the exam is 40. We advise you to first solve questions that you find easier. You can use reasonably high-level mathematical proofs except in part 4.3 where we will need an explicit sequence of proof steps. If you are running out of time on a particular problem, try to convince us that you know the right strategy to solve it. Reminder: If t ⊆ B × B is a binary relation and C ⊆ B, we define
t[C] = {y | ∃x ∈ C. (x,y) ∈ t}
The diagonal relation on C ⊆ B is ∆C = {(x,x) | x ∈ C}. Given t1,t2 ⊆ B × B, relation composition ◦ is:
t1 ◦ t2 = {(x,z) | ∃y.(x,y) ∈ t1 ∧ (y,z) ∈ t2}
Reflexive transitive closure of t is
t∗ = [ti
i≥0
where t0 = ∆B, t1 = t, tn+1 = t ◦ tn. If M = (S,I,r,A) is a transition system we define
r¯ = {(s,s′) | ∃a ∈ A.(s,a,s′) ∈ r}
and define the reachable states as image of I under the reflexive transitive closure of ¯r:
Reach(M) = ¯r∗[I]
Do not open the exam until we tell you to.
1 Transition Systems and Invariants (8pt)
Let M = (S,I,r,A) be a transition system with I ⊆ S and I ̸= ∅ a non-empty initial set of initial states, r ⊆ S × A × S the transition relation and A the (non empty) input alphabet.
Part I. For each of the following, prove or give a counter-example.
1.1 Diagonal
If ¯r is the diagonal relation, then every subset of S is an inductive invariant.
1.2 Lurking Havoc
If there exists an s1 ∈ S such that for all s2 ∈ S, (s1,s2) ∈ r¯, then the smallest inductive invariant is S.
1.3 Rock Star
For any s2: if for all s1 ∈ S we have (s1,s2) ∈ r¯, then s2 ∈ Reach(M). Stated as a formula:
∀s2.((∀s1 ∈ S.(s1,s2) ∈ r¯) −→ s2 ∈ Reach(M))
1.4 Transitions over a Lattice
If S is a complete lattice with the order relation ≤ and with the greatest lower bound of a set denoted by d, then if for all s1,s2, (s1,s2) ∈ r¯ → s1 ≤ s2, then for u = dI, the set Iu = {s ∈ S | u ≤ s} is an inductive invariant.
1.5 No Junk
If, for all s ∈ S I, ¯r[{s}] ⊆ Reach(M), then every invariant is an inductive invariant.
∗∗∗∗
Part II. In the following parts, for any set of initial states I′ ⊆ S and relation r′ ⊆ S×A×S, let M(I′,r′) denote the transition system (S,I′,r′,A) and let Reach(I′,r′) denote Reach(M(I′,r′)). For each of the following, prove or give a counter-example.
1.6 One Reach, Two Reaches
For any r1, r2 and I, Reach(Reach(I,r1),r2) ⊆ Reach(I,r1 ∪ r2).
1.7 Both Reach
For any r1, r2 and I, Reach(I,r1 ∪ r2) ⊆ Reach(Reach(I,r1),r2).
1.8 Invariant Part by Part
For any r1, r2 and I, if i1 is an invariant of M(I,r1) and i2 is an invariant of M(I,r2) then i1 ∪ i2 is an invariant of M(I,r1 ∪ r2).
2 Quantifier Elimination (5pt)
These problems can be solved using the technique of quantifier elimination for linear arithmetic that we studied in the lectures. You can skip steps when transforming quantifier-free sub-formulas into equivalent ones. You can use your own strategy for applying quantifier elimination steps.
2.1 An Integer Formula
Consider the formula F(x,z) where the variables range over the mathematical integers Z:
∀y.((x < y ∧ y < z) −→ (3 | (y + 1) ∨ 3 | (y + 2)))
(3 | (y + 1) stands for “3 divides (y + 1)”.)
Find a quantifier-free formula equivalent to F(x,z).
2.2 A Rational Arithmetic Formula
Consider the following formula G(x,z) where the variables range over rational numbers Q:
∀y.((x < y ∧ y < z) −→ ∀u.(x ̸= u + u + u))
Find a quantifier-free formula equivalent to G(x,z).
3 Programs and Formulas (9pt)
Consider a program with two variables ranging over unbounded integers Z, so let S = Z2 be the set of possible states of the program at a program point.
3.1 Program to Formula
Convert the following program into a formula that expresses the program’s meaning:
x= x + y if x > y then
x= x − y
else
y= y − x
Your formula should have:
1. x,y,x′,y′ as the only free variables
3. no relations or functions other than those of integer linear arithmetic.
3.2 About That Program
Let r ⊆ S ×S be the semantics of the program in the previous part. Consider the initial set of states p:
p = {(x,y) ∈ S | 0 ≤ x + y}
Find the formula that describes the strongest postcondition of p with respect to r. Specifically, compute a quantifier-free formula Q containing as the variables only x and y, such that the set
q = {(x,y) | Q}
is the relation image of set p under relation r, that is, q = r[p] holds.
You do not need to show detailed steps, but be careful to give a formula for the exact relation image (strongest postcondition).
3.3 Quadratic Mess
This part is solvable independently of the previous two. Consider the initial set of states
p = {(x,y) ∈ S | x2 ≤ y}
Let r ⊆ S ×S now be the meaning of the following program with two assignments executed one after another:
y= y − 1 x= x + y
Compute a quantifier-free formula Q containing as variables only x and y that characterizes the strongest postcondition of p with respect to r, that is, a formula Q such that the set
q = {(x,y) | Q}
is the relation image of set p under relation r, that is, q = r[p] holds.
4 First Order Logic Resolution (7pt)
Consider the following first order logic signature L = {E,a,f,g}, consisting of a binary relation symbol E, a constant a, a function f taking 1 argument, and a function g taking 1 argument. Recall that, in FOL, we distinguish terms (denoting values in the domain) from formulas (denoting truth values).
4.1 Defining Terms
Let V denote a countable set of variables used to build terms and formulas. Let T denote the set of all terms with variables V in the signature L. Let GT denote the set of ground terms corresponding in the signature L (domain of the Herbrand universe).
a) Does g(f(a)) belong to GT?
b) Does g(f(x)) belong to GT?
c) Does E(f(a),a) belong to GT?
d) Does E(f(x),a) belong to T?
e) Give a definition for a function H : 2T → 2T such that these two conditions hold:
T = [Hi(V )
i≥0
GT = [Hi(∅)
i≥0
Do not use GT in the definition of H. (This way, we can use H to define GT.)
(Hi(x) denotes the iterated application of H, i.e., H0(x) = x, Hi+1(x) = H(Hi(x)).)
4.2 Axioms and Their Normal Form
Consider the following formula A:
∀x,y,z. (E(x,y) ∧ E(y,z) → E(x,z)) ∧
(E(x,y) → (E(f(x),f(y)) ∧ E(g(x),g(y)))) ∧ E(f(g(x)),g(f(x)))
Show the result of transforming the above formula into an equivalent finite set of first-order clauses.
4.3 Applying Resolution
Use the clauses obtained in the previous part to show that E(f(f(g(a))),g(f(f(a)))) is a consequence of formula A.
E(f(f(g(a))),g(f(f(a)))) as E(ffga,gffa).
5 The Age of AI - Abstract Interpretation (11pt)
For simplicity, consider programs with a single variable. A set of states is a subset of the set of integers, so the concrete domain is the set of all subsets, C = 2Z. The ordering on concrete elements is ⊆, which gives a (complete) lattice with the least upper bound ∪ and the greatest lower bound ∩.
The abstract domain elements are four-tuples (a,b,c,d) where a,b,c,d can be integers and where a can also be −∞ and b can also be +∞. We assume that −∞ ≤ x and x ≤ +∞ for every x ∈ Z. Hence,
A = {(a,b,c,d) | a ∈ {−∞} ∪ Z,b ∈ Z ∪ {+∞},c,d ∈ Z}
Define
γ(a,b,c,d) = {x | a ≤ x ≤ b ∧ ∃k ∈ Z. x = kd + c}
5.1 Special Case
Give a simple definition of the set γ(a,b,0,1) and for the set γ(a,a,0,1).
5.2 Abstract Strongest Postcondition for Assignment
Consider the following assignment statement c1:
x = x - 3
Let r1 ⊆ Z2 be the meaning of that statement. Write down an expression defining r1.
Then, give a definition of a function such that, for all x ∈ A,
)) (1)
Try to define F1# such that γ(F#(x)) is as small set as possible while satisfying the above condition.
Illustrate your definition by showing and simplifying the mathematical expression for F#((a,a,0,1)) where a ∈ Z.
5.3 Abstract Strongest Postcondition for Tests
Analogously to the previous part, consider the command c2:
assume(x > 3)
whose meaning is relation r2. Give functions that satisfies the condition analogous to (1):

Also give that corresponds to the command:
assume(x <= 3)
5.4 Joining
Propose a definition of J : A × A → A such that for all x,y:
• J(x,y) = J(y,x)
• γ(x) ⊆ γ(J(x,y))
and such that γ(J(x,y)) is as small as you can make it while satisfying the above two conditions.
5.5 Loop and Its Control-Flow Graph
// 1 x = 20 while // 2
x > 3 do
// 3
x = x − 3
// 4
Draw a control flow diagram with these 4 program points, with edges labeled by assignments and tests (“assume” statements).
Let I1 be the mathematical formula “true”.
Find formulas I2,I3,I4 expressible in the language of integer linear arithmetic with the divisibility operator such that I1,I2,I3,I4 result in valid Hoare triples according to the control flow graph, and such that they are as strong as you can make them (making all of them “true” is not a good solution).
For example, the following should be valid Hoare triples (among others):
• I1 {x = 20} I2
• I2 {assume(x > 3)} I3
• I3 {x = x - 3} I2
5.6 Injectivity
Give an example showing that γ is not injective.
Define a subset AN ⊆ A such that γ restricted to AN is injective and γ[AN] = γ[A]. We write γN for the restriction of γ to AN: γN(x) = γ(x) for all x ∈ AN.
5.7 Ordering on A
Define a binary partial order relation ≤ on AN such that γN is an injective monotonic function from AN to C.
5.8 Galois Insertion
Can you define α : C → AN such that (α,γN) form a Galois insertion between C and AN?
(Reminder: a Galois insertion is a Galois connection where γN is injective.)
End of the Exam Sheet