MI-FME Formalni metody a specifikace

• http://cs.cas.cz/~ratschan
• stefan.ratschan at cs.cas.cz
• FIT 319

• A ∧ T ⇔ A
• A ∧ F ⇔ F
• A ∨ T ⇔ T
• A ∨ F ⇔ A
• A ∧ B ⇔ B ∧ A
• A ∨ B ⇔ B ∨ A
• A ∧ (B ∨ C) ⇔ (A ∧ B) ∨ (A ∧ C)
• A ∨ (B ∧ C) ⇔ (A ∨ B) ∧ (A ∨ C)
• ¬¬ A ⇔ A
• ¬ (A ∧ B) ⇔ ¬ A ∨ ¬ B
• ¬ (A ∨ B) ⇔ ¬ A ∧ ¬ B
• (A ⇔ B) ⇔ (A ⇒ B ∧ B ⇒ A)
• (A ⇒ B) ⇔ (¬ B ⇐ ¬ A)
• (A ⇔ B) ⇔ (¬ B ⇔ ¬ A)

• ∃ x. ∃ y.A ⇔ ∃ y. ∃ x.A
• ∀ x. ∀ y.A ⇔ ∀ y. ∀ x.A
• ¬∀ x.A je ⇔ ∃ x. ¬ A
• ¬∃ x.A je ⇔ ∀ x. ¬ A
• ∀ x . A ∧ B ⇔ [ ∀ x.A] ∧ [ ∀ x.B]
• ∃ x . A ∨ B ⇔ [ ∃ x.A] ∨ [ ∃ x.B]
• ∀ x . A ∨ B ⇔ [ ∀ x.A] ∨ B pokud B neobsahuje x
• ∃ x . A ∧ B ⇔ [ ∃ x.A] ∧ B pokud B neobsahuje x

• A je ekvivalentní A
• Pokud A je ekvivalentní B pak B je ekvivalentní A
• Pokud A je ekvivalentní B, a B je ekvivalentní C pak A je ekvivalentní C

• A ⇒ B je zkratka pro ¬ A ∨ B
• A ⇔ B je zkratka pro A ⇒ B ∧ B ⇒ A

Z toho plyne:

• A ⇒ B je ekvivalentni ¬ B ⇐ ¬ A
• A ⇔ B je ekvivalentni ¬ B ⇔ ¬ A

• A ∧ B: Nejdřív dokážeme A, pak B
• A ∨ B: Předpokládáme ¬ A a dokážeme B
• A ⇒ B: Předpokládáme A a dokážeme B.
• ¬ A: Předpokládáme A a zkusíme najít rozpor. Rozpor: Situace kdy pro určité P, P i ¬ P jsou známé skutečnosti.

• A ∧ B: Usoudíme i A i B
• A ∨ B: Píšeme nejdřív ”Případ A :”, předpokládáme A a dokončíme důkaz. Pak píšeme ”Případ B :”, předpokládáme B, a dokončíme důkaz.
• A ⇒ B: Pokud známe A pak usoudíme B
• ¬ A: Pokud už hledáme spor, pak místo ¬A dokazujeme A.

• ∃ x . A: Vybereme (intuicí, kreativitou) term t, a dokážeme A[x ← t]
• ∀ x . A: Vybereme novou konstantu a, píšeme ”Nechť a je libovolné ale pevné” a dokážeme A[x ← a]
• A ∧ B: Nejdřív dokážeme A, pak B
• A ∨ B: Předpokládáme ¬ A a dokážeme B
• A ⇒ B: Předpokládáme A a dokážeme B.
• ¬ A: Předpokládáme A a zkusíme najít rozpor

• ∃ x . A: Vybereme novou konstantu a, píšeme ”necht’ a je tak, že A[x ← a]”, a přiřadíme A[x ← a] do našeho seznamu známých skutečností.
• ∀ x . A: Vybereme (intuicí, kreativitou) term t a usoudíme A[x ← t]
• A ∧ B: Usoudíme A i B
• A ∨ B: Píšeme nejdřív ”Případ A :”, předpokládáme A a dokončíme důkaz. Pak píšeme ”Případ B :”, předpokládáme B, a dokončíme důkaz.
• A ⇒ B: Pokud známe A pak usoudíme B
• ¬ A: Pokud už hledáme spor, pak místo ¬A dokazujeme A.

∀x ∀x' . [I (x) ∧ x' = f (x)] ⇒ O(x, x')

• cons : T × L → L
• first : L → T
• rest : L → L
• empty : → L

• ∀ l, x . first(cons(x, l)) = x
• ∀ l, x . rest(cons(x, l)) = l
• ∀ l, x . l ≠ empty() ⇒ cons(first(l), rest(l)) = l
• ∀ l, x . cons(x, l) ≠ empty()
• Chování first(empty()), rest(empty()) není specifikováno.

• · [·] : A n × { 1, . . . , n } → T
• write : A n × { 1, . . . , n } × T → A n

• ∀ a, v, i, j . i = j ⇒ write(a, i, v)[j] = v
• ∀ a, v, i, j . i ≠ j ⇒ write(a, i, v)[j] = a[j]
• ∀ a, b . [ ∀ i . a[i] = b[i]] ⇔ a = b

• 0 : → N
• 1 : → N
• + : N × N → N
• · : N × N → N

• ∀ x . x + 1 ≠ 0
• ∀ x, y . x + 1 = y + 1 ⇒ x = y
• ∀ x . x + 0 = x
• ∀ x, y . x + (y + 1) = (x + y) + 1
• ∀ x . x0 = 0
• ∀ x, y x(y + 1) = xy + x

Pro každou formuli F s přesně jednou volnou proměnnou x, další axiom

• [ F[x ← 0] ∧ [∀ x . F ⇒ F [x ← x + 1] ] ] ⇒ ∀ x . F

• αi ⇒ αl

• αi ⇒ αi+1[v ← v0]

• [[αi ∧ P] ⇒ αi+1] ∧ [[αi ∧ ¬ P] ⇒ αl ]

@ α
  v1 ← t1; . . . ; vn ← tn
@ α'

• α ⇒ α'[vn ← tn] . . . [v1 ← t1]

!!Pozor na posloupnost přiřazení!!

@ α
while P do
  @β
  . . .
  @β'
@ α'

• [α ∧ P] ⇒ β
• [α ∧ ¬ P] ⇒ α'
• [β' ∧ P] ⇒ β
• [β' ∧ ¬ P] ⇒ α'

@ α
for i ← l to u
  @β
  . . .
  @β'
@ α'

• [α ∧ l ≤ u] ⇒ β[i ← l]
• [α ∧ l > u] ⇒ α'
• [β' ∧ i < u] ⇒ β[i ← i + 1]
• β'[i ← u] ⇒ α'