Obsah

AP5, IN5 Důkazy programů
Diskuze

AP5, IN5 Důkazy programů

Zadání

(dokazování vlastností programů, induktivní metody, invarianty cyklů)

Vypracování

Označení

(Tato část je napsána podle slajdů k předmětu Návrh algoritmů 1.)

Označení

In Množina vstupních dat.
Out Množina výstupních dat.
A : In → Out Algoritmus.
$\varphi: In \mapsto Bool$ vstupní podmínka
$\psi: In \times Out \mapsto Bool$ výstupní podmínka

Intuitivně řečeno, vstupní podmínka je unární predikát na množině vstupních dat a vymezuje ty, se kterými je algoritmus „ochoten pracovat“. Výstupní podmínka říká, zda daný výstup je, nebo není výstupem algoritmu pro daný vstup. Pomocí těchto podmínek vyjadřujeme formálně svoje tvrzení o chování programu. Podmínky nemusí popisovat úplně celé chování programu, popisují jen to, co chceme dokazovat.

Příklad

Algoritmus A přečte tři čísla a vypíše je v neklesajícím pořadí. Funguje korektně jen pro nezáporná čísla.

In = Out = $\mathbb{Z}\times\mathbb{Z}\times\mathbb{Z}$
$\varphi_A((x,y,z))$ je true právě když $x \geq 0 \wedge y \geq 0 \wedge z \geq 0$
$\psi_A(((x,y,z), (u,v,w)))$ je true právě když (u,v,w) je permutací (x,y,z) a $u\leq v\leq w$

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.

Tvrzení, která budeme dokazovat

Definice 1

Říkáme, že algoritmus A je konvergentní vzhledem k $\varphi$ , pokud je množina $\left\{x\in In | \varphi(x)\right\}$ podmnožinou definičního oboru funkce A.

Intuitivně toto znamená, že algoritmus je konvergentní, pokud zastaví pro každou hodnotu povolenou vstupní podmínkou.
(definiční obor algoritmu A jsou právě ty vstupy, pro které zastaví, to víme z vyčíslitelnosti).

Příklad 1

Pokud tedy tvrdíme, že algoritmus zastaví pro libovolné přirozené číslo na vstupu (tedy tvrdíme, že $\varphi(x) = true \Longleftrightarrow x \in \mathbb{N}$ ) a přitom se program zacyklí pro vstup 14, potom náš program není konvergentní vzhledem k $\varphi$ .

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

Definice 2

Řekneme, že A je parciálně korektní vzhledem k $\varphi, \psi$ , pokud pro každou vstupní
hodnotu x z definičního oboru funkce A, pro kterou $\varphi(x) = true$ , platí
$\psi((x, A(x)))$

Intuitivně tedy musí algoritmus dávat ty hodnoty, které předepisuje výstupní podmínka $\psi$ . Ale stačí, když je bude dávat jen pro vstupy povolené vstupní podmínkou $\varphi$ . Navíc tato podmínka nepředepisuje, že algoritmus musí zastavit. Pokud tedy bude cyklit pro jakýkoliv vstup, stejně bude parciálně korektní.

A nakonec definice, která říká to, co opravdu od programu očekáváme:

Definice 3

Řekneme, že A je totálně korektní vzhledem k $\varphi, \psi$ , když je konvergentní vzhledem k $\varphi$ a parciálně korektní vzhledem k $\varphi, \psi$ .

Jinak řečeno algoritmus musí skončit pro každou hodnotu povolenou vstupní podmínkou $\varphi$ a navíc musí dát hodnotu splňující výstupní podmínku $\psi$ .

Důkazové techniky

Nyní se dostaneme k tomu, jak vlastně dokázat, že program je totálně korektní vzhledem ke vstupní a výstupní podmínce. Důkazové techniky jsou trochu jiné pro funkcionální a pro imperativní paradigma.

Funkcionální paradigma

Dokazování vlastností čistě funkcionálních programů je jednodušší, protože každá funkce má nějakou hodnotu, o které můžeme něco tvrdit. Nejčastější důkazová technika je indukce, která často dobře odpovídá definicím funkcí v Haskellu.

Příklad funkcionálního programu 1

Mějme v Haskellu funkci/program fact fact 0 = 1

 fact n = n * fact (n - 1)

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

Program fact je konvergentní vzhledem ke vstupní podmínce $\varphi$ , která je definována $\varphi(x) = True \Leftrightarrow x\in \mathbb{N}_0$ .
Program fact je parciálně korektní vzhledem k výstupní podmínce $\psi$ , která je definována $\psi((x, y)) = True \Leftrightarrow y = x!$

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 $x \in \mathbb{N}_0$ , 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 $\psi((0, 1)) = True$ .
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)!.

Příklad funkcionálního programu 2

Funkce maxim najde největší číslo z konečného neprázdného seznamu čísel.

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 $\psi$ bude definována jako $\psi\left(\left((a_0, a_1, ..., a_n) , \;x\right)\right) = True \Leftrightarrow \left(\forall i \in \left\{1, ... n\right\}\right)(x \geq a_i)$

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 $(a_0)$ délky 1 tvrzení triviálně platí.
Indukční krok: Předpokládáme, že tvrzení platí pro posloupnost $(a_n,... a_1, a_0)$ a dokážeme ho pro posloupnost $(a_{n+1}, a_n, ... a_0)$ kde $n \geq 1$ . Seznamy jsou řazeny stejně jako seznamy v Haskellu. Uvážíme dvě možnosti.

$a_{n+1} > a_n$ . Potom výsledkem bude maxim (a_n+1, a_{n - 1}, … a₀). 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ý.

Příklad funkcionálního programu 3

A nakonec algoritmus třídění vkládáním.

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.

Imperativní paradigma

Zde je situace trochu složitější. Pokud máme v imperativním jazyce napsán program funkcionálním stylem, například

int fact(int x) { 
  if (x == 0) 
    return 1; 
  else 
    return x * fact(x - 1); 
}

potom můžeme použít stejnou techniku jako pro funkcionální paradigma.

V ostatních případech využijeme mezilehlé podmínky a invariant cyklu.

Důkaz konvergentnosti imperativních programů spočívá obvykle v nalezení číselné hodnoty, která v žádném okamžiku výpočtu nemůže být záporná a přitom při každém průchodu tělem cyklu klesne nejméně o jedničku. ¹⁾

Mezilehlá podmínka je tvrzení, jehož platnost v určitém místě programu dokážeme a potom ho použijeme k dokázání další mezilehlé podmínky, invariantu cyklu nebo nakonec výstupní podmínky. Jinými slovy, mezilehlá podmínka je takový záchytný bod v programu. Mezilehlé podmínky umístíme na místa, v nichž se stav výpočtu významně mění nebo kde není zcela zřejmá správnost programu ²⁾

Příklad - mezilehlá podmínka

Uvažme následující pseudokód algoritmu třídění haldou:

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.

Pokud náš algoritmus pracuje nad nějakou datovou strukturou, potom obvykle vyslovíme podmínku, kterou datová struktura před a po běhu algoritmu vždy splňuje. Tuto podmínku pak využijeme k důkazu správnosti algoritmu. Samozřejmě pro algoritmy modifikující datovou strukturu musíme dokázat i to, že po jeho běhu podmínka stále platí. Tato podmínka datové struktury se obvykle formuluje ve vstupní a výstupní podmínce algoritmu.

Příklad - invariant datové struktury

Mějme například binární vyhledávací strom a na něm následující algoritmus:

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.

Algoritmy obvykle obsahují cykly. Pro dokázání jejich správnosti používáme invariant cyklu.
Invariant cyklu je mezilehlá podmínka umístěná v cyklu. Můžeme ho umístit, kam potřebujeme, ale musíme vždy dokázat následující:

Z předpokladů platících před cyklem (tedy buď ze vstupní podmínky algoritmu nebo z mezilehlých podmínek) dokážeme, že invariant cyklu platí při prvním běhu.
Je-li splněn invariant cyklu a cyklus se provede, potom invariant cyklu opět platí.
Je-li splněn invariant cyklu a cyklus skončí (není splněna podmínka cyklu), potom je splněna mezilehlá podmínka za cyklem nebo výstupní podmínka algoritmu.

Příklad - invariant cyklu 1

Následující imperativní program v Pascalu dokážeme pomocí invariantu cyklu:

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 i₀ hodnotu proměnné i před provedením cyklu a i₁ hodnotu proměnné i po jednom provedení cyklu. Podobně zavedeme i k₀ a k₁. Podle definice programu bude platit i₁ = i₀ + 1 a k₁ = k₀ * i₁. Dle předpokladu tedy k₁ = i₀! * i₁ = i₁!. 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!.

Příklad - invariant cyklu 2

Algoritmus umocňování pomocí půlení exponentu v Pascalu:

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 y^k = zⁿ, 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*y^k = zⁿ ∧ k ≥ 0. Dokážeme už jen hlavní část důkazu korektnosti.

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

Pokud je k₀ sudé, potom r₁ = r₀, k₁ = k₀ / 2, y₁ = y₀². Potom $r_1 y_1^{k_1} = r_0 \left(y_0^2\right)^{\frac{k_0}{2}} = r_0 y_0^{k_0} = z^n$ dle předpokladu.
Je-li k₀ liché, potom $r_1 = r_0 y_0, k_1 = \frac{k_0 - 1}{2}, y_1 = y_0^2$ . Potom je $r_1 y_1^{k_1} = r_0 y_0 \left(y_0^2\right)^{\frac{k_0 - 1}{2}} = r_0 y_0 y_0^{k_0 - 1} = r_0 y_0^{k_0} = z^n$ opět dle předpokladu, že před provedením těla platil invariant cyklu.

Na konci je k = 0 a proto y^k = 1 a proto r = zⁿ a proto je splněna výstupní podmínka.

Příklad - invariant cyklu 3

Algoritmus řazení vkládáním v Pascalu.

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_1 \leq ... A_{j-1} \leq A_j = A_{j+1} \leq A_{j+2} \leq ... A_i$ 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 A_j ≤ x, bude hodnota x vložena na správné místo a invariant vnějšího cyklu bude opět splněn.

Induktivní metody

(Tato část je napsána podle učebního textu k předmětu Úvod do informatiky)

Nejen správnost programu často dokazujeme pomocí indukce. A i takový invariant cyklu je vlastně indukce. Pro důkaz indukcí existuje několik technik.

Fixace parametru

Pokud má program více parametrů, ale jeden z nich se nemění, nemusíme se o něj v indukci starat a vlastnost dokážeme obecně pro jakoukoliv hodnotu tohoto parametru.

Příklad - fixace parametru

Mějme následující funkci implementující násobení přirozených čísel:

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.

Indukce k součtu parametrů

Tuto techniku potřebujeme použít v případě, kdy máme více parametrů, které se postupně zmenšují, ale pokaždé je to jiný z nich.

Příklad - součet parametrů

Mějme následující funkci

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ý.

Zesílení dokazovaného tvrzení

Toto je často používaná indukční důkazová technika. Při důkazu indukcí potřebujeme mít dostatečně silný indukční předpoklad, abychom se od něho mohli „odpíchnout“ a dokázat další krok. Proto může být nutné dokázat silnější tvrzení, ze kterého potom naše požadované tvrzení triviálně vyplývá.

Příklad - zesílení dokazovaného tvrzení

Uvažme následující definice:

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 = 2^x. 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.

Předměty

IB002 Návrh algoritmů 1 RNDr. Libor Škarvada
IB000 Úvod do informatiky doc. RNDr. Petr Hliněný Ph.D.

Literatura

Zápisky k přednášce Návrh algoritmů 1, RNDr. Libor Škarvada
Skripta k IB000 Úvod do informatiky doc. RNDr. Petr Hliněný Ph.D.

Zpracování

Vypracovává Roman Plášil, quiark@mail.muni.cz

Materiál je převzat ze slidů předmětu Návrh algoritmů 1. Ty jsou trochu strohé, proto jsem se snažil látku vysvětlit podle toho, jak ji chápu já a tedy doufám, že ji chápu dobře. Dále se omlouvám všem, pro které je vysvětlení příliš zdlouhavé, ale myslím, že se najde dost lidí, pro které je tato oblast těžko uchopitelná a jim to doufám pomůže. Uvítám připomínky a opravy, pokud něco nechápete, napište.

Poznámka k označení: Výstupní podmínku píšu se dvojitými závorkami ve tvaru ψ( (x, y) ), protože jde o funkci na uspořádané dvojici a toto je čistě formální zápis. Zápis s jedinou závorkou je ale používán častěji. Podobně je to se zápisem φ(x) = True ⇔ podmínka. Vstupní podmínka se dá chápat jako podmnožina množiny In, přestože je to ve skutečnosti funkce. Já se držím zápisu odpovídajícímu definici, ale množinový zápis by se asi taky dal tolerovat. A nakonec k označování proměnných v části převzaté z textu k IB000. Volně zaměnuji proměnnou v programu a proměnnou v důkazu, čímž se odlišuji od zdrojového textu a jeho formálních definic.

Stav zpracování: z mé strany hotovo.

¹⁾

Slidy Návrh algoritmů 1, str.14

²⁾

Pokud bychom chtěli dokázat správnost naprosto formálně, do posledního bitu, museli bychom mít k dispozici formální sémantiku daného jazyka a potom bychom umístili mezilehlou podmínku mezi každé dva příkazy a všechny bychom dokázali. To se ovšem ze zřejmých důvodů v praxi moc nedělá.

Diskuze

Petr Kott, 2008/06/13 14:09

Pěkně zpracované. Mám jen jeden dotaz, nemá u toho deklarativního (Pascal) faktoriálu být vstupní podmínka In(x) = True ⇔ x náleží Z (Tj. celým číslům). Odkazuješ se na funkcionální verzi, tam se ale u záporných čísel zacyklíš, tady ne.
Dík za odpověď

Roman Plášil, 2008/06/14 10:34

Nemá, protože vstupní podmínka nepopisuje všechny hodnoty, pro které program skončí, ale jen ty, pro které bude splněna výstupní podmínka. Navíc faktoriál pro záporná čísla není definován. Dále podmínky si můžu zvolit podle sebe, podle toho, co chci dokazovat. Pokud bych chtěl dokázat jen to, že ta funkce spočítá správně faktoriál jedničky a dvojky, potom vstupní podmínka bude obsahovat 1, 2 a výstupní podmínka bude {(1, 1), (2, 2)}. Trochu jsem to dovysvětlil v textu.

Petr Kott, 2008/06/16 00:53

jasné jasné.. máš pravdu. Jsem mysel, že podmínku neurčuješ ty, ale určuje se, podle konkrétního programu, kdy se nezacyklí.

Dusan Katona, 2008/06/14 19:44

Otazka je spracovana velmi pekne, mam ale taky maly dotaz:
V skriptach z Uvodu do informatiky je tiez kapitola „Dokazovani vlastnosti programu“, nie je to take formalne ako z navalu I, su tam ale popisane rozne induktivne metody (fixace parametru, indukce k souctu parametru), nemysli sa tymi „induktivnymi metodami“ v zadani prave toto?

Roman Plášil, 2008/06/14 20:44

Jo, to je možné :) Tak já se na to podívám. Jen nevím, jestli mám někde štrachat skripta prof. Kučery, nebo stačí od doc. Hliněného.

Dusan Katona, 2008/06/14 20:53

Tie od prof. Kucery uz na nete nie su, ak ich nenajdes, tak ja ich mam v pdf, napis mi ked tak na icq…Do skript doc. Hlineneho som sa nepozeral..

Hanáček, 2008/06/16 17:12

Nemá v imperativní verzi faktoriálu místo „na začátku běhu je k = 1 a i = 1“ být i=0. Aspoň to tak mám ve skriptech.

Roman Plášil, 2008/06/16 17:34

Tak jo :)

Ludvík Vidlák, 2008/06/18 13:17

Kdy bude tato otazka prohlasena za hotovou?

Tomáš Hanáček, 2008/06/19 22:03

Asi by bylo dobré nějak zdůraznit že Algoritmus je parciální fce, tady to vypadá že je totální, pak by ale definice konvergence neměla smysl.Pokud to chápu dobře.

Jitka Pospíšilová, 2008/06/19 23:31

Tato otázka je velmi dobre zpracovana, tuto tematiku jsem nikdy moc dobre nechapala, ale diky vsem intuitivnim vysvetlenim v tom mam uz celkem jasno. Autorovi moc diky za skvele zpracovani :)

Ondřej Božek, 2008/06/20 20:38

Nějak se mi nezdá ta definice konvergence vzhledm k phi , konkretně { x in In | phi(x)} .

Roman Plášil, 2008/06/21 11:02

Přesně takhle je to na slidech. Mě to přijde v pořádku.

Ondřej Božek, 2008/06/20 21:21

Důkaz funkce maxim:
…
-An+1>An … (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{ne, má délku n!}, my dokazujeme pro seznam délky n + 2{ne, pro seznamy délky n+1!}) …

Je to tak?

Roman Plášil, 2008/06/21 11:07

Podle mě není, seznam (a_0, a_1, … a_(n-1), a_(n+1)) má n + 1 prvků.

Petr Koutný, 2008/06/21 10:57

Hodně pěkně vypracovaná otázka, díky!

Karel Barot, 2008/06/22 05:07

Mohl by mne nekdo prosim potvrdit/vyvratit nasledujici:

Definicni obor algoritmu A je mnozina hodnot pro ktere algoritmus zastavi, ale vysledek nemusi byt spravny?
(vzdy jsem si myslel, ze vysledek byt spravny musi)

„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.“
Takze pokud do nej vlozim zaporne cislo, tak algoritmus zastavi, ale nevypise spravny vysledek? Jaky je definicni obor tohoto algoritmu? Cela cisla, nebo jen nezaporna?

Diky moc

Roman Plášil, 2008/06/22 12:44

Definiční obor funkce je množina, pro kterou je funkce definována, pro ostatní čísla je výsledek neznámý = nedefinovaný. Podobně je to u algoritmu, pokud pro daný vstup algoritmus něco vrátí, pak je hodnota pro ten vstup definována (aneb víme, co vrátí). Pokud cyklí donekonečna, potom nevíme, co vrátí, a tudíž je návratová hodnota nedefinovaná.

Jestli vrátí tu hodnotu, jakou chceme, je už jiná věc.

Martin Minář, 2008/06/23 15:39

>„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.“
Takze pokud do nej vlozim zaporne cislo, tak algoritmus zastavi, ale nevypise spravny vysledek? Jaky je definicni obor tohoto >algoritmu? Cela cisla, nebo jen nezaporna?

Pokud to spravne chapu, tak podle toho co popisujes jsou def. oborem tohoto algoritmu cela cisla, tedy za podminky, ze algoritmus zastavi pro kazde cele cislo. Ale pokud je vstupni podminka omezena na No, tak algoritmus bude pro zaporna cisla vracet spatne hodnoty. Nebo lepe, nemas zaruceno, ze vysledek bude spravny.
Ale stejne tak muzes muzes do algoritmu s def oborem No vlozit hodnotu zapornou a algoritmus, resp. program spadne, zacykli, ci se bude jinak nedeterministicky chovat.

You could leave a comment if you were logged in.

home/inf/ap5.txt · Poslední úprava: 2020/04/12 16:56 (upraveno mimo DokuWiki)

Nahoru