TU Wien:Programm- und Systemverifikation VU (diverse)/Suggested-Solution-Exam-SS18

1.) Coverage (6 + 9 + 2 + 3 Points)

(a)

	satisfied
Criterion	yes	no
statement coverage	x
branch coverage	x
decision coverage		x
modified condition/decision coverage		x

decision coverage: (result || tmp) is never false

MC/DC: (result || tmp) is never false

(b)

	satisfied
Criterion	yes	no
all-defs	x
all-c-uses		x
all-p-uses		x
all-c-uses/some-p-uses		x
all-p-uses/some-c-uses		x

all-c-uses: result = result || tmp never used in result || tmp; also no loop-free def-clear path from result = false to result = result || tmp

all-p-uses: m = n never used in i % m == 0

all-p-uses/some-c-uses: follows from all-p-uses

all-c-uses/some-p-uses: follows from all-c-uses

(c)

all-p-uses
Inputs		Outputs
m	n	result
7	3	true

all-c-uses
Inputs		Outputs
m	n	result
1	3	true

(d)

MC/DC
Inputs			Outcome	Affected condition
a	b	c	(a && b) || c
0	1	0	0	if a flips we get true
1	0	0	0	if b flips we get false
0	0	1	1	if c flips we get false
1	1	0	1	if either a or b flips we get false
0	0	0	0	if c flips we get true

??? If anyone is certain whether 000 is correct please provide an explanation here: ???

2) Hoare Logic (10 Points)

{true}

{true} (consequence rule; simplify pre-condition)

{0 = (n − n) · m} (assignment rule)

x := n;

{0 = (n − x) · m} (assignment rule)

y := 0;

{y = (n − x) · m} (from conditional rule)

if (m != 0) {

{(m != 0) ∧ (y = (n − x) · m)} (consequence; strengthen pre-condition y = (n − x) · m)

{y = (n − x) · m} (loop invariant from loop rule)

while (x != 0) {

{y = (n − x) · m} (consequence rule, is equal to expression below)

{y = (n − x + 1) · m − m} (consequence rule, is equal to expression below)

{y + m = (n − (x − 1)) · m} (assignment rule)

x = x - 1;

{y + m = (n − x) · m} (assignment rule)

y = y + m;

{y = (n − x) · m}

}

{(x = 0) ∧ (y = (n − x) · m)} (loop rule)

{(y = n · m)} (consequence rule)

} else {

{(m = 0) ∧ (y = (n − x) · m)} (consequence; strengthen pre-condition)

{(y = n · m)} (skip rule) [(m = 0) ∧ (y = n * m)]

skip;

{(y = n · m)}

}

{(y = n · m)} (conditional rule)

{y = n · m}

3.) Invariants (10 Points)

• (x ≤ 100) ∧ (y ≤ 100): Non-inductive invariant. Invariant since program terminates with x = y = 100. Non-inductive, since successor of x = 50 and y = 100 violates the assertion.
• (y - x) ≤ 50: Inductive Invariant. Base case holds (x = 0, y = 50). Induction step: x is always increased by 1, y only every second time, therefore the difference (y-x) can only become smaller and was already smaller or equal than 50.
• x != y: Neither, Program terminates with x = y = 100, which violates the assertion.

4.) Temporal Logic (5 + 5 Points)

a)

1. AXa - {s₂}
2. EXa - {s₀, s₁, s₂}
3. AFb - {s₀, s₁}
4. EGa - {s₀, s₁, s₂}
5. A(a U b) - {s₀}

b)

1. LTL formula AFGa - {s₀, s₁, s₂}
2. CTL formula AFAGa - {s₀, s₁, s₂}

Do the formulas (i) and (ii) above express the same property?

Yes.

5.) Decision procedures (5 + 5 Points)

a)

1) p ∧ q ∧ (¬p ∨ ¬q ∨ r) ∧ (¬r ∨ ¬t) ∧ (t ∨ s) ∧ ¬s ➔ No solution, p ∧ q ∧ r ∧ ¬t ∧ s !! but this can't be since ¬s is also asked for.

2) (x ∨ y) ∧ (¬x ∨ ¬y) ∧ (y ∨ z) ∧ (¬y ∨ ¬z) ∧ (z ∨ x) ∧ (¬z ∨ ¬x) ➔

➔ No solution:

• Decision Level 1 ¬x → ¬x ∧ z ∧ y !! this can't be since ¬y would also be needed.
• Decision Level 0 x → x ∧ ¬y ∧ z !! this can't be since ¬z would also be needed.

3) (¬x ∨ y) ∧ (x ∨ ¬y) ∧ (¬y ∨ z) ∧ (y ∨ ¬z) ∧ (z ∨ ¬z) ➔ Solution: ¬x ∧ ¬y ∧ ¬z

4) q ∧ (¬r ∨ ¬q) ∧ t ∧ (t ∨ ¬t ∨ r) ∧ (¬t ∨ r) ➔ No solution, q ∧ ¬r ∧ t !! but this can't be since ¬t is also asked for.

5) (x ∨ y) ∧ (¬x ∨ ¬y) ∧ (y ∨ ¬z) ∧ z ∧ (¬x ∨ z) ➔ Solution: z ∧ y ∧ ¬x

b) Tseitin transformation

Construct an equi-satisfiable formula: You introduce a new variable for each of the subformulas. Then rewrite them into CNF. You get subformulas with only constant blowup.