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:
For the second, you need to recognize that the outcome of
max(i, j)
will be computed along one of two paths: one, wheni<j
and the other wheni>=j
(the logical negation ofi<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 ofmax(i, j)