Formal Methods, Logic and VDM past exam paper questions

Question

I was hoping someone can help me with the following questions, answers would be best but if you can point me in the right direction that will be helpful also. I am a final year uni student and these questions are from a previous exam on Formal Methods and I could do with knowing the answers ready for this years paper. Our lecturer does not seem the best and has not covered a lot of this and so finding the exact answer has been proving impossible. Google has not been much of a help nor has the recommended books.

1 - Given that ∃x • P (x) is logically equivalent to ¬∀x • ¬P (x) and that ∀x ∈ S • P (x) means ∀x • x ∈ S ⇒ P (x), deduce that ∃x ∈ S • P (x) means ∃x • x ∈ S ∧ P (x)

2 - Describe the two statements that would have to be proved to show that the definition:

max(i, j)
if i>j
then i
else j

is a correct implementation of the specification:

max(i : Z, j : Z)r : Z
pre true
post (r = i ∨ r = j) ∧ i ≤ r ∧ j ≤ r

Answer 1

The first is really just manipulation of symbols using the given and two other well-known logical equivalences:

(1) ∃x • P(x) is logically equivalent to ¬∀x • ¬P(x)
(2) ∀x∈S • P(x) means ∀x • x∈S ⇒ P(x)

∃x∈S • P(x)
== ¬∀x∈S • ¬P(x) (from (1))
== ¬∀x • x∈S ⇒ ¬P(x) (from (2))
== ¬∀x • ¬x∈S v ¬P(x) (from def. of ⇒)
== ¬∀x • ¬(x∈S ∧ P(x)) (from ¬A v ¬B == ¬(A ∧ B))
== ∃x • x∈S ∧ P(x) (from (1) -- the other way around)

For the second, you need to recognize that the outcome of max(i, j) will be computed along one of two paths: one, when i<j and the other when i>=j (the logical negation of i<j)

So you need to show that

1. if true ∧ i<j (precondition), then (r=i ∨ r=j) ∧ i≤r ∧ j≤r (post condition), and
2. if true ∧ i>=j (precond.) then (r=i ∨ r=j) ∧ i≤r ∧ j≤r (post cond.),

where r is the result of max(i, j)

Answer 2

But section 2 of your question does not make sense since any implementation that returns either i or j is correct.

The specification is wrong.

A correct postcondition is

post (i > j => r = i) v (i <= j => r = j)