Ako som už niekoľkokrát spomínal, vývoj softvéru je transformácia požiadaviek zákazníka na funkčný softvér. V zásade by to nemusel byť problém, ak by to nebol proces viacfázový, dlhodobý a nezúčastňovalo sa ho viacero rôznych profesií alebo tímov. Ak by sa aj pominuli všetky tieto komplikácie, tak tu ostáva ešte samotná komplikovanosť celého procesu, kde je potrebné skĺbiť rôzne požiadavky (funkčnosť, rýchlosť, bezpečnosť atď.). Čerešničkou na torte je, že keď sa konečne z ohňa softvérovej vyhne vynorí ukutý softvér, môže byť tak komplikovaný, že overiť ho voči pôvodným požiadavkám nie je vôbec triviálne. Práve na riešenie takýchto problémov vznikli formálne metódy.

Jedným zo spôsobov, ako udržať vývoj softvéru v smere, za ktorý si platí zákazník, je použiť agilné metódy. Tesný kontakt so zákazníkom a časté uvoľňovanie softvéru dokáže robiť divy a výsledok môže byť naozaj to, čo zákazník skutočne potrebuje (to nemusí byť to isté, ako to, o čom na začiatku hovoril – ale to už je iný príbeh). Aj keď som očitým svedkom toho, že agilné metódy dokážu celkom v pohode zvládať veľké dlhodobé projekty a radím sa medzi ich zástancov, nie je to strieborná guľka, s ktorou zastrelíte každé monštrum. Napríklad takým cestujúcim v Parížskom metre na linke 14 by sa v momente, keď ich vlak zastaví mimo stanice, asi len ťažko vysvetľovalo, že oprava príde v najbližšej aktualizácii. Celá tá linka je totiž riadená automaticky – bez šoféra. Toto riadenie je pekným prípadom pre safe-critical systémy. To sú také, kde chyba v produkčnej prevádzke môže stáť niekoho život. A práve na takého prípady sú tu formálne metódy (pre dané metro je to konkrétne B-metóda).

Čo to teda formálne metódy sú? Je to množina postupov a nástrojov na zápis, transformáciu a overenie požiadaviek na ľubovoľný systém (ja budem ďalej hovoriť o systéme softvérovom). To znamená, že pomocou nich dokážem požiadavky zapísať, následne ich viem postupne transformovať na hotový kód a na záver ešte výsledný systém spätne overiť voči požiadavkám. A to pomocou striktných matematických nástrojov (nie náhodou sú formálne metódy deťmi informatiky, ktorá má korene v matematike). Práve v tom, že je to takýto ucelený systém a v tej striktnosti je najväčšia sila týchto nástrojov. Vďaka tomu totiž bude dodaný softvér, ktorý spĺňa počiatočné požiadavky. Stráca sa vágnosť, ktorá sa môže objaviť pri ústnom podaní alebo pri písanom texte, prípadne neformálnych diagramov. Všetko je navrhnuté tak, aby do seba zapadalo.

Formálnych metód je strašne veľké množstvo. Dá sa povedať, že denne vznikajú nové prispôsobením existujúcich pre nejaké konkrétne požiadavky. Veľké množstvo z nich sa pravdepodobne nikdy neuplatní v praxi (čo ale neznamená, že nemajú svoju hodnotu). Medzi najznámejšie patria Petriho siete, Procesná algebra alebo B-metóda. Takú formálnu metódu si tak trochu viete predstaviť ako programovací jazyk. Na jednej strane obsahuje nejakú syntax zápisu alebo notáciu kreslenia. Na druhej strane potom nástroje pre prácu s týmto zápisom. Napríklad viete vytvoriť model systému a potom tomuto modelu posielať vstupy a sledovať, čo sa so systémom deje. Tak si viete otestovať funkčnosť systému pred jeho implementáciou alebo porovnať existujúci systém s týmto modelom. Dôležité je, že z toho modelu viete veľa vlastností systému odvodiť matematickými operáciami. A teda vám formálna metóda môže dať odpoveď napríklad na otázku, či sa systém dostane do nejakého konkrétneho stavu (či už žiadaného alebo chybového).

Ak máte pocit, že stále neviete presne, o čom hovorím, ale pritom máte strednú alebo vysokú školu technického smeru, tak veľmi pravdepodobne ste už s jednou formálnou metódou robili a asi ani o tom neviete. Ak ste mali nejaký predmet, ktorý súvisel so slaboprúdovou technikou pravdepodobne ste preberali aj Boolovu algebru. Aj ona je považovaná za formálnu metódu. Konkrétne na vývoj číslicových obvodov. Najprv sa zadefinuje správanie výstupov na základe vstupov a potom sa pomocou vzorcov robia transformácie, až sa dôjde k zapojeniu konkrétnych číslicových obvodov. Podstatné na tom je práve to, že ak ste pri tom odvodzovaní – transformácii – dodržiavali pravidlá, tak výsledný systém bol v správaní de facto totožný s tým, čo ste mali na začiatku, len zápis sa zmenil tak, že ste vedeli podľa neho vyrobiť celé zapojenie. A takto nejako formálne metódy fungujú. Len pre iné prípady systémov a iné scenáre použitia.

Ak je to všetko také super, kde je problém? Prečo sa nepoužívajú formálne metódy denne? Je to kvôli ich zložitosti. Aby ste ich vedeli používať, musíte ich dobre poznať – mal by ich poznať každý v tíme. Ideálne, ak s nimi vie pracovať zákazník. A to nie je málo. Taktiež znižujú pružnosť. Malá zmena požiadaviek môže znamenať prepočítať celý systém. Ak sa vrátim k príkladu s Boolovou algebrou, tak zmena jedného výstupného pinu na číslicovom obvode sa nedá zapracovať inak, ako znovuodvodením celého systému. A to všetko znamená, že formálne metódy sú drahé. Preto sa používajú len tam, kde je to nutné (Boolová algebra je trochu výnimka, pretože je pomerne jednoduchá).