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
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
true ∧ i<j (precondition), then (r=i ∨ r=j) ∧ i≤r ∧ j≤r (post condition), andtrue ∧ i>=j (precond.) then (r=i ∨ r=j) ∧ i≤r ∧ j≤r (post cond.),where r is the result of max(i, j)