Správnost programů
Z FAV wiki
(Rozdíly mezi verzemi)
(Založena nová stránka: Testováním programu, tj. ověřením, že pro daný vstup získáme správný výsledek, nemůžeme obecně prokázat správnost programu. Množství vstupů je většino...) |
m (kategorizace) |
||
| (Nejsou zobrazeny 3 mezilehlé verze od 1 uživatele.) | |||
| Řádka 1: | Řádka 1: | ||
Testováním programu, tj. ověřením, že pro daný vstup získáme správný výsledek, nemůžeme obecně prokázat správnost programu. Množství vstupů je většinou tak veliké, že testování není možné ani za použití velice rychlých počítačů. Na druhé straně testování může alespoň prokázat chybu v programu. Protože empirickým testováním nemůžeme zaručit správnost programu, musíme ho nahradit analytickým přístupem pro porozumění správnosti programu. Sekvence příkazů (přiřazení, alternativy a cyklu) umožňuje dokázání správnosti programu tak, že můžeme napsat tvrzení o hodnotách proměnných před vykonáním příkazu, které nazýváme předpoklad a tvrzení po jeho vykonání, které nazýváme důsledek. | Testováním programu, tj. ověřením, že pro daný vstup získáme správný výsledek, nemůžeme obecně prokázat správnost programu. Množství vstupů je většinou tak veliké, že testování není možné ani za použití velice rychlých počítačů. Na druhé straně testování může alespoň prokázat chybu v programu. Protože empirickým testováním nemůžeme zaručit správnost programu, musíme ho nahradit analytickým přístupem pro porozumění správnosti programu. Sekvence příkazů (přiřazení, alternativy a cyklu) umožňuje dokázání správnosti programu tak, že můžeme napsat tvrzení o hodnotách proměnných před vykonáním příkazu, které nazýváme předpoklad a tvrzení po jeho vykonání, které nazýváme důsledek. | ||
| − | Příkazy sekvenčně | + | |
| + | == Příkazy sekvenčně == | ||
| + | |||
Například pokud máme dva příkazy sekvenčně za sebou, tak vyjdeme z požadovaného | Například pokud máme dva příkazy sekvenčně za sebou, tak vyjdeme z požadovaného | ||
důsledku druhého příkazu. Na základě důsledku stanovíme požadovaný předpoklad pro druhý | důsledku druhého příkazu. Na základě důsledku stanovíme požadovaný předpoklad pro druhý | ||
| Řádka 7: | Řádka 9: | ||
vstupů. | vstupů. | ||
| − | Příkazy alternativy | + | |
| + | == Příkazy alternativy == | ||
| + | |||
Příkazy alternativy zachovávají sekvenční vykonávání příkazu. | Příkazy alternativy zachovávají sekvenční vykonávání příkazu. | ||
| − | Příkazy cyklu | + | |
| + | == Příkazy cyklu == | ||
| + | |||
Pro pochopení příkazů opakování zavedeme pojem invariant cyklu. | Pro pochopení příkazů opakování zavedeme pojem invariant cyklu. | ||
Pro invariant cyklu musíme obecně ukázat tři vlastnosti: | Pro invariant cyklu musíme obecně ukázat tři vlastnosti: | ||
| − | + | * '''Inicializace''' - je splněn před vykonáním prvního cyklu. | |
| − | + | * '''Udržování''' - je-li splněn pře vykonáním cyklu, zůstává splněn i po něm. | |
| − | + | * '''Skončení''' - když příkaz cyklu skončí, invariant nám ukáže správnost algoritmu (dokážeme-li, že inicializace platí, a cyklus je udržován pro všechny iterace). | |
Přiklad na řazeni pole vkládáním: | Přiklad na řazeni pole vkládáním: | ||
| − | Inicializace: Po začátečním přiřazení i = 1 je pole s prvky s indexy 0, ..., i-1 | + | * '''Inicializace''': Po začátečním přiřazení i = 1 je pole s prvky s indexy 0, ..., i-1 osahující jeden prvek triviálně seřazeno. |
| − | osahující jeden prvek triviálně seřazeno. | + | * '''Udržování''': Cyklus while posouvá již seřazené prvky a[i-1], a[i-2], ... o jednu pozici doprava dokud se nenajde správné místo pro a[i]. Výsledkem je, že prvky pole a[0] ... a[i] jsou seřazeny. Invariant je tedy splněn i pro následující opakování, kdy i je v hlavičce cyklu inkrementováno. |
| − | Udržování: Cyklus while posouvá již seřazené prvky a[i-1], a[i-2], ... o jednu pozici | + | * '''Skončení''': Cyklus for skončí když i=n, kde n je počet prvků pole. Dosazením do textu invariantu cyklu dostáváme, že prvky s indexy 0 ... n-1 obsahují seřazené původní prvky pole, co je to co jsme požadovali. |
| − | doprava dokud se nenajde správné místo pro a[i]. Výsledkem je, že prvky pole a[0] ... a[i] | + | |
| − | jsou seřazeny. Invariant je tedy splněn i pro následující opakování, kdy i je v hlavičce | + | |
| − | cyklu inkrementováno. | + | {{fav-kiv-bzinf}} |
| − | Skončení: Cyklus for skončí když i=n, kde n je počet prvků pole. Dosazením do | + | [[Kategorie:fav-kiv-bzinf]] |
| − | textu invariantu cyklu dostáváme, že prvky s indexy 0 ... n-1 obsahují seřazené původní | + | |
| − | prvky pole, co je to co jsme požadovali. | + | |
Aktuální verze z 20. 2. 2014, 06:34
Testováním programu, tj. ověřením, že pro daný vstup získáme správný výsledek, nemůžeme obecně prokázat správnost programu. Množství vstupů je většinou tak veliké, že testování není možné ani za použití velice rychlých počítačů. Na druhé straně testování může alespoň prokázat chybu v programu. Protože empirickým testováním nemůžeme zaručit správnost programu, musíme ho nahradit analytickým přístupem pro porozumění správnosti programu. Sekvence příkazů (přiřazení, alternativy a cyklu) umožňuje dokázání správnosti programu tak, že můžeme napsat tvrzení o hodnotách proměnných před vykonáním příkazu, které nazýváme předpoklad a tvrzení po jeho vykonání, které nazýváme důsledek.
[editovat] Příkazy sekvenčně
Například pokud máme dva příkazy sekvenčně za sebou, tak vyjdeme z požadovaného důsledku druhého příkazu. Na základě důsledku stanovíme požadovaný předpoklad pro druhý příkaz, což je také požadovaný důsledek pro první příkaz atd. až získáme hodnoty možných vstupů.
[editovat] Příkazy alternativy
Příkazy alternativy zachovávají sekvenční vykonávání příkazu.
[editovat] Příkazy cyklu
Pro pochopení příkazů opakování zavedeme pojem invariant cyklu. Pro invariant cyklu musíme obecně ukázat tři vlastnosti:
- Inicializace - je splněn před vykonáním prvního cyklu.
- Udržování - je-li splněn pře vykonáním cyklu, zůstává splněn i po něm.
- Skončení - když příkaz cyklu skončí, invariant nám ukáže správnost algoritmu (dokážeme-li, že inicializace platí, a cyklus je udržován pro všechny iterace).
Přiklad na řazeni pole vkládáním:
- Inicializace: Po začátečním přiřazení i = 1 je pole s prvky s indexy 0, ..., i-1 osahující jeden prvek triviálně seřazeno.
- Udržování: Cyklus while posouvá již seřazené prvky a[i-1], a[i-2], ... o jednu pozici doprava dokud se nenajde správné místo pro a[i]. Výsledkem je, že prvky pole a[0] ... a[i] jsou seřazeny. Invariant je tedy splněn i pro následující opakování, kdy i je v hlavičce cyklu inkrementováno.
- Skončení: Cyklus for skončí když i=n, kde n je počet prvků pole. Dosazením do textu invariantu cyklu dostáváme, že prvky s indexy 0 ... n-1 obsahují seřazené původní prvky pole, co je to co jsme požadovali.
