Správnost programů - Historie editací

Acolade: kategorizace

2014-02-20T06:34:08Z

kategorizace

← Starší verze		Verze z 20. 2. 2014, 06:34
Řádka 30:		Řádka 30:

	{{fav-kiv-bzinf}}		{{fav-kiv-bzinf}}
		+	[[Kategorie:fav-kiv-bzinf]]

Tester: /* Příkazy cyklu */

2011-08-24T17:11:07Z

Příkazy cyklu

← Starší verze		Verze z 24. 8. 2011, 17:11
Řádka 27:		Řádka 27:
	* '''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 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.		* '''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.
		+
		+
		+	{{fav-kiv-bzinf}}

Tester: /* Příkazy cyklu */

2011-08-07T15:35:49Z

Příkazy cyklu

← Starší verze		Verze z 7. 8. 2011, 15:35
Řádka 25:		Řádka 25:
	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 osahující jeden prvek triviálně seřazeno.		* '''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]	+	* '''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.
−	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.		* '''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.

Tester v 7. 8. 2011, 15:35

2011-08-07T15:35:29Z

← Starší verze		Verze z 7. 8. 2011, 15:35
Řá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.	+	* '''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.	+	* '''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).	+	* '''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]
−	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		jsou seřazeny. Invariant je tedy splněn i pro následující opakování, kdy i je v hlavičce
	cyklu inkrementováno.		cyklu inkrementováno.
−	Skončení: Cyklus for skončí když i=n, kde n je počet prvků pole. Dosazením do	+	* '''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.
−	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.	+

Tester: 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...

2011-08-03T15:14:47Z

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

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š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ě
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ů.

Příkazy alternativy
Příkazy alternativy zachovávají sekvenční vykonávání příkazu.

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.