Table of Contents

MI-FME Formalni metody a specifikace

Ekvivalence

Pravidla ekvivalence:

Implikace, ekvivalence

Z toho plyne:

Důkazní pravidla

Jak zjednodušovat to, co chceme dokázat?

Jak produkovat nové známé věci?

Jak zjednodušovat to, co chceme dokázat?

Jak produkovat nové známé věci?

Správnost algoritmu

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

Axiomatizace seznamů

Funkční symboly

Axiomy (l ∈ L , x ∈ T ):

Axiomatizace polí

Funkční symboly:

Axiomy (a, b ∈ A n, v ∈ T , i, j ∈ { 1, . . . , n } ):

Axiomatizace přirozených čísel

Funkční symboly:

Axiomy (Peanova aritmetika)

Indukce

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

Aserce

goto l

input v

if P then

v ← t

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

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

while

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

for

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