AP5, IN5 Důkazy programů

• In = Out =
• je true právě když
• je true právě když (u,v,w) je permutací (x,y,z) a

Tedy vstupní podmínka říká, že algoritmus funguje jen pro nezáporná čísla, přestože do něj můžeme
vložit i záporné číslo. Výstupní podmínka říká, jak bude vypadat výstup, pokud vstup splňuje vstupní podmínku.

Stačí z vyřadit 14 a jsme v suchu ;)

 fact n = n * fact (n - 1) 

Vyslovíme o ní následující dvě tvrzení:

• Program fact je konvergentní vzhledem ke vstupní podmínce , která je definována .
• Program fact je parciálně korektní vzhledem k výstupní podmínce , která je definována

Konvergentnost dokážeme z demonstračních důvodů indukcí.
Bázový krok: Pro x = 0 program podle definice skončí.
Indukční krok Dokazujeme, že pokud program skončí pro , potom skončí i pro x + 1. Z definice programu vidíme, že se volá funkce fact pro n - 1 = x a jinak se provádí jen jedno sčítání a jedno násobení. Sčítání ani násobení se nezacyklí a konvergentnost funkce fact pro x máme z indukčního předpokladu. Tedy ani pro x + 1 se program fact nezacyklí.

Zkráceně bychom mohli říct, že je zřejmé, že n se vždy o 1 zmenší a proto program skončí.

Parciální korektnost opět indukcí, tentokrát to vezmeme trochu rychleji.
Bázový krok: Pro x = 0 je z definice faktoriálu zřejmé, že .
Indukční krok: Předpokládáme platnost tvrzení pro x, dokážeme ho pro x + 1. Dosazením do definice fact x + 1 = (x + 1) * fact x a s použitím indukčního předpokladu je fact x + 1 = (x + 1) * x!. Podle definice faktoriálu je i fact x + 1 = (x + 1)!.

maxim [x] = x 
maxim (x:y:s) = if x > y then maxim(x:s) 
                         else maxim(y:s) 

In, Out v tomto případě budou seznamy (posloupnosti) čísel. Vstupní podmínka bude platná pro neprázdné konečné seznamy, výstupní podmínka bude definována jako

Konvergentost je zřejmá, neboť při každém rekurzivním volání funkce maxim se sníží délka seznamu o 1 a pro seznamy délky 1 funkce vždy skončí.

Parciální korektnost dokážeme indukcí vzhledem k délce seznamu.
Bázový krok: Pro posloupnost délky 1 tvrzení triviálně platí.
Indukční krok: Předpokládáme, že tvrzení platí pro posloupnost a dokážeme ho pro posloupnost kde . Seznamy jsou řazeny stejně jako seznamy v Haskellu. Uvážíme dvě možnosti.

• . Potom výsledkem bude maxim (an+1, an - 1, … a0). Můžeme použít indukční předpoklad, protože je to seznam o 1 prvek kratší (má délku n + 1, my dokazujeme pro seznam délky n + 2) a proto víme, že výsledkem bude maximální prvek posloupnosti (a_n+1, a_{n - 1}, … a₀). Ten je zároveň maximálním prvkem posloupnosti (a_n+1, a_n, a_{n - 1}, … a₀), protože prvek a_n není maximální.
• Druhý případ je analogický.

inssort [] = [] 
inssort (x:s) = ins x (inssort s) 
  where ins x [] = [x] 
        ins x (y:t) = if x <= y then x:(y:t) 
                                else y:(ins x t) 

Množinou všech vstupů i výstupů budou všechny posloupnosti čísel. Vstupní podmínka omezí vstupy jen na konečné posloupnosti a výstupní podmínka platí pro (x, y) právě tehdy, když y je permutací posloupnosti x a y je neklesající.

Abychom mohli dokázat totální korektnost funkce inssort, musíme dokázat totální korektnost funkce ins, protože ta je při výpočtu inssort používána. Její vstupní množinou je dvojice (x, A), kde x je číslo a A je posloupnost čísel. Tato funkce ke své správné funkci vyžaduje, aby byl seznam A neklesající. Vstupní podmínka tedy je φ( (x, A) ) = True ⇔ A je konečná a neklesající. Výsledkem této funkce je opět neklesající seznam A, do kterého byl vložen prvek x na příslušné místo. Tedy ψ( ( (x, A), B ) ) = True ⇔ B je neklesající, B obsahuje x a B obsahuje všechny prvky, které obsahuje A.

Nejprve dokážeme totální korektnost funkce ins. Konvergentnost je zřejmá z předpokladu, že každý seznam na vstupu je konečný a že při každém rekurzivním volání se velikost seznamu zmenší o 1 a funkce pro prázdný seznam triviálně skončí. Indukční krok důkazu parciální korektnosti rozdělíme na dvě možnosti:

• Je-li x ≤ y, potom je výsledkem funkce seznam x:y:t. Pro něj zřejmě platí, že obsahuje všechny prvky jako seznam y:t, dále zřejmě platí, že obsahuje i prvek x. Rovněž platí, že je neklesající, protože seznam y:t je dle vstupní podmínky neklesající a x ≤ y.
• Jinak je výsledkem seznam y:(ins x t). Tento seznam také splňuje všechny podmínky, protože dle IP je ins x t neklesající, obsahuje prvek x a všechny prvky z t. Tedy i seznam y:(ins x t) obsahuje všechny prvky jako seznam y:t, prvek x a navíc je díky IP a tomu, že y < x, neklesající.

Přejdeme k důkazu funkce inssort. Konvergentnost je opět zřejmá z toho, že na vstupu jsou pouze konečné seznamy, že funkce ins je konvergentní a že při každém rekurzivním volání inssort je předán seznam o 1 prvek kratší. Parciální korektnost se dokáže opět indukcí vzhledem k délce seznamu. Indukční krok říká, že můžeme aplikovat ins x (inssort s), protože dle IP je s neklesající seznam. Dostaneme neklesající seznam, ve kterém budou všechny prvky z s a prvek x. To je ale seznam, který splňuje výstupní podmínku funkce inssort a proto jsme hotovi.

int[] heapsort(int []A) 
  H = prázdná halda 
  pro každý prvek x v A 
    vlož x do haldy H 
 
  * 
     
  B = prázdný seznam 
  dokud H není prázdná: 
    vyber nejmenší prvek m z H 
    přidej m do B 
   
  vrať B 

Zde bychom použili mezilehlou podmínku na místě označeném hvězdičkou. Tato podmínka by říkala, že H obsahuje všechny prvky ze seznamu A a má vlastnost haldy, tedy že pro každý uzel X platí: je-li Y synem uzlu X, potom X ≤ Y. Jakmile bychom dokázali, že kód před hvězdičkou opravdu takovou haldu vytvoří, mohli bychom to použít k důkazu toho, že kód za hvězdičkou skutečně vytvoří uspořádaný seznam.

int getmin(Node n) 
  if n nemá levého syna 
    return n.hodnota 
  else 
    return getmin(n.left) 

Jeho správnost dokážeme snadno použitím invariantu BVS, který říká, že pro každý uzel X stromu platí, že všechny uzly v jeho levém podstromu mají menší hodnotu než X a všechny uzly v pravém podstromu mají větší hodnotu než uzel X.

function factorial(n: Integer): Integer; 
var i, k: Integer; 
begin 
  i := 0; 
  k := 1; 
  while i < n do begin 
    i := i + 1; 
    k := k * i; 
  end; 
  factorial := k; 
end; 

Vstupní a výstupní podmínku už formulovat nebudu, každý si ji jistě dokáže vymyslet sám a navíc je stejná jako pro funkcionální verzi faktoriálu. Ukončení cyklu v algoritmu je zřejmé z toho, že proměnná i vždy vzroste o 1 a proměnná n je konstantní a proto jednou musí i být větší nebo rovno n. Parciální korektnost dokážeme s pomocí invariantu cyklu k = i! ∧ 0 ≤ i ≤ n v místě testování podmínky cyklu.

• Na začátku běhu je k = 1 a i = 0. Tedy platí k = i!. Druhá část invariantu zřejmě platí také.
• Předpokládejme, že invariant platí. Označme i0 hodnotu proměnné i před provedením cyklu a i1 hodnotu proměnné i po jednom provedení cyklu. Podobně zavedeme i k0 a k1. Podle definice programu bude platit i1 = i0 + 1 a k1 = k0 * i1. Dle předpokladu tedy k1 = i0! * i1 = i1!. Dále zřejmě platí i 0 ≤ i ≤ n. Tím je dokázána platnost invariantu.
• Po ukončení cyklu platí k = i! = n!.

function power(z: Real; n: Integer): Real; 
var y, r: Real 
    k: Integer; 
begin 
  k := n; 
  y := z; 
  r := 1; 
  
  while k > 0 do begin 
    if odd(k) then r := r * y; 
    k := k div 2; 
    y := y * y; 
  end; 
  power := r; 
end; 

Zde už máme o něco složitější algoritmus a invariant cyklu není zřejmý na první pohled. Je vidět, že při každém zmenšení k na polovinu se umocní y na druhou. Proto dokud se dá k dělit na poloviny beze zbytku, je yk = zn, protože y obsahuje dosavadní umocněnou hodnotu a k říká, jak moc ještě musíme umocňovat. Když je k liché, zaokrouhlí se při dělení 2 směrem dolů a tak se jakoby přeskočí jedno umocnění. Kvůli tomu je tam proměnná r, do které se přinásobují mocniny z vždy, když je dělení k nepřesné (= když je k liché). Invariant cyklu je tedy r*yk = zn ∧ k ≥ 0. Dokážeme už jen hlavní část důkazu korektnosti.

Předpokládejme, že je invariant splněn. Označíme si y0, y1, k0,… podobně jako v minulém příkladu.

• Pokud je k0 sudé, potom r1 = r0, k1 = k0 / 2, y1 = y02. Potom dle předpokladu.
• Je-li k0 liché, potom . Potom je opět dle předpokladu, že před provedením těla platil invariant cyklu.

Na konci je k = 0 a proto yk = 1 a proto r = zn a proto je splněna výstupní podmínka.

const MAX = 999; 
type Posl = array [1..MAX] of Integer; 
procedure InsSort(n:Integer; var A: Posl); 
var i, j, x:Integer; 
begin 
  for i := 2 to n do begin 
    x := A[i]; 
    j := i - 1; 
    while (j > 0) and (A[j] > x) do begin 
      A[j + 1] := A[j]; 
      j := j - 1; 
    end; 
    A[j + 1] := x; 
  end; 
 end; 

Nalezení invariantů cyklu jde u tohoto algoritmu ruku v ruce s pochopením jeho funkce. Musíme si v duchu projít několik prvních kroků, abychom viděli, jak vypadá a jak se mění seznam A vlivem algoritmu. Ve vnějším cyklu vidíme, že se vezme i-tý prvek, uloží se do x a na konci se někam vloží. Místo, kam se vloží, hledá vnitřní cyklus – postupuje od pozice i - 1 směrem k začátku seznamu a skončí až když najde hodnotu menší než x. Zároveň s tím přerovnává všechny prvky o jednu pozici doprava, aby x mohlo být do seznamu vloženo. Tímto způsobem se postupně buduje uspořádaný seznam.

Invariant vnějšího cyklu je, že prvních i-1 prvků v seznamu A je seřazených, zbývající prvky jsou ve stejném pořadí jako ve vstupním seznamu a seznam A obsahuje všechny prvky jako vstupní seznam. Invariant vnitřního cyklu je a prvních i prvků seznamu A je permutací prvních i prvků vstupního seznamu.

Platí-li invariant vnějšího cyklu, potom platnost invariantu vnitřního cyklu je zřejmá – cyklus kopíruje prvky o jednu pozici doprava. Dále jelikož je dle předpokladu prvních i-1 seřazených a vnitřní cyklus skončí jakmile Aj ≤ x, bude hodnota x vložena na správné místo a invariant vnějšího cyklu bude opět splněn.

mul 0 _ = 0 
mul x y = y + mul (x - 1) y 

Důkaz, že jde skutečně o násobení má následující tvar. Nechť n ∈ N je libovolné, ale dále pevné. Dokážeme běžnou indukcí vzhledem k m, že pro každé m ∈ N je mul m n = m * n.

g 0 _ = 0 
g _ 0 = 0 
g x y = g (x - 1) y + g x (y - 1) 

Chceme dokázat, že pro každé m, n ∈ N platí g m n = 0. Nemůžeme použít klasickou indukci k m nebo n, protože ani u jednoho nemáme zaručeno, že se vždy zmenší. Ale vždy se zmenší alespoň jeden a proto můžeme vést důkaz vzhledem k součtu parametrů. Dokážeme tedy tvrzení
Pro každé i ∈ N platí, že jestliže i = m + n pro libovolná m, n ∈ N, potom g m n = 0.
Z tohoto tvrzení potom přímo vyplyne platnost výstupní podmínky.

Bázový krok:
Na začátku i = 0. Z toho plyne, že m = n = 0 a platnost tvrzení je triviální.
Indukční krok:
Zde uvážíme tři možnosti.

• m = 0. Potom zřejmě g 0 n = 0.
• m > 0, n = 0. Opět zřejmě g m 0 = 0.
• m > 0, n > 0. Dle definice platí g m n = (g (m - 1) n) + (g m (n - 1)). Nyní můžeme použít indukční předpoklad na g (m - 1) n, protože součet parametrů je menší než i. Podobně použijeme IP i na g m (n - 1). Zbytek je zřejmý.

f 0 = 1 
f x = h x 
h 0 = 1 
h x = f (x - 1) + h (x - 1) 

Chceme dokázat, že pro každé x je h x = 2x. To ale nelze dokázat indukcí přímo, protože bychom neměli k dispozici žádné tvrzení o funkci f. Proto musíme zesílit tvrzení na
Pro každé n ∈ N platí f n = 2ⁿ a h n = 2ⁿ.
Toto tvrzení už dokážeme snadno.