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, protože množství různých vstupů je až na triviální případy tak veliké, že toto není možné ani použitím velice rychlých počítačů. Na druhé straně testování může 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. Dále si ukážeme tento postup na příkladech.
Nejprve se zabývejme sekvencí dvou příkazů přiřazení obr. a položme si otázku, kdy bude tento fragment programu počítat správně. Při analýze sekvence příkazů obecně vyjdeme z požadovaného důsledku vykonání posledního (v našem případě druhého) příkazu určíme předpoklad správného vykonání, který je zase požadovaným důsledkem předcházejícího příkazu atd. až nakonec učíme, jaké tvrzení musí platit pro vstupy programu, aby pracoval správně.
V našem příkladě na obr. důsledkem druhého příkazu je obecné tvrzení
y >= 0
Na to, aby důsledkem přiřazení hodnoty výrazu e proměnné v, bylo tvrzení Q(v), musí být splněn předpoklad Q(e). Jinými slovy, to co má platit pro proměnnou v, muselo platit pro výraz e, kterého hodnotu ji přiřadíme. Toto pravidlo je jenom formální vyjádření, chceme-li definice, účinku přikazu přiřazení. V našem případě je požadovaný předpoklad Öx >= 0 a po úpravě x >= 0. Opakováním tohoto postupu, získáme požadovaný předpoklad pro první příkaz přiřazení, tedy x - 1 >= 0 a x >= 1. Dokázali jsme tedy, že uvedený program bude správně počítat pro x >= 1.
V sekvenci příkazů dobře strukturovaného programu se ovšem vyskytují také příkaz alternativy pro výběr jednoho z příkazů a příkaz cyklu pro opakování sekvence příkazů. Pro správnost programů je důležité vyjádřit účinek těchto příkazů známe-li účinek jednotlivých příkazů uvnitř příkazů alternativy a cyklu.
Uvažujme problém nalezení větší ze dvou hodnot x a y. Výsledná hodnota proměnné m má být x je-li x ≥ y a y je-li x < y. Fragment programu opisující uvedený výpočet je na obr. .
Příkaz alternativy vykoná přiřazení m=x je-li splněna podmínka x >= y a příkaz m=y v opačném případě. Můžeme tedy říct, že po jeho vykonání bude platit tvrzení
(x >= y && m == x) || (!(x>=y) && m==y)
a po malé úpravě
(x >= y && m ==x) || (x<y) && m==y)
co je právě to co jsme požadovali
Pro pochopení příkazů opakováni používáme pojem invariant cyklu. Ukážeme si ho na příkladu řazení vkládáním na obr..
Algoritmus pracuje tak, že prvek s indexem i v cyklu for vkládá do uspořádané začáteční části pole a[0], ..., a[i-1], tedy jemu předcházejících prvků. Vskutku, prvky a[0], ..., a[i-1] obsahují původní hodnoty těchto prvků, jenomže nyní seřazené. Tuto vlastnost nazýváme invariantem cyklu, kterou můžeme formulovat následovně.
Na začátku každého vykonávání cyklu for, začátek pole s prvky s indexy 0, ..., i-1 obsahuje hodnoty původních prvků, jenomže seřazené.
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.
Z prvních dvou vlastností plyne, že invariant cyklu je splněn před každým vykonáním cyklu. Tento postup je podobný matematické indukci, kdy dokazujeme platnost tvrzení pro základní případ a pro indukční krok. Splnění invariantu před prvním vykonáním cyklu odpovída základnímu případu a udržování odpovídá indukčnímu kroku. Třetí vlastnost odlišuje inavariant cyklu od matematické indukce, indukce končí nastane-li podmínka pro skončení cyklu. Z pohledu správnosti programů, spojením podmínky skončení cyklu a invariantu cyklu dostáváme tvrzení platné po skonční cyklu.
Ukažme si uvedené vlastnosti pro invariant cyklu v algoritmu řazení 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 for 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.
Z uvedených příkladů, které zahrnují všechny řídící konstruce programovacího jazyka, je v první řadě zřejmé, že i když programování je kreativní činnost a D.Knuth ji v nadpise svého několikasvazkového díla "The Art of Programming" označil jako umění, lze program exaktně zkoumat a vyslovit tvrzení platná o průběhu jeho vykonávaní. Tato lze chápat jako přesné komentáře programu a tak jako z důvodu srozumitelnosti nedáváme komentáře ke každému příkazu, nýbž jenom na důležitá místa kódu, stejně tak je vhodné postupovat v případě tvrzení. Často je uvádíme právě v komentářích. Mezi důležitá tvrzení patří zejména invarianty cyklů a předpoklad a důsledek metod, včetně metody main( ). V případě objektového programování je dále vhodné uvádět invariant objektu, což je tvrzení platné pro jeho členské proměnné bez ohledu na počet a pořadí volání jeho metod.
Novější programovací jazyky jako C, C++, Java, C# obsahují příkaz assert, ve kterém můžeme zapsat tvrzení, kterého platnost na daném místě kódu požadujeme. Pokud při vykonávání programu je jeho platnost porušena, jsme na tuto skutečnost upozorněni.