Untitled

Formal Methods, Logic and VDM past exam paper questions
max(i, j)
if i>j
then i
else j

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

(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)