Formální metody

Specifikace softwarového systému může být formální nebo neformální. Neformální specifikace používá přirozený jazyk, případně obrázky, tabulky a ostatní nástroje umožňující pochopit popisovaný systém. V okamžiku, kdy taková notace získává charakter precizní syntaxe i sémantiky, stává se formální specifikaci. Formální specifikace je technika umožňující jednoznačně specifikovat softwarový systém. Často hovoříme také o semiformálních metodách, které mají přesně danou syntaxi, ale netrváme na úplné a precizní sémantice - patří sem jazyk UML.

Cílem formálních metod není jen jednoznačně systém popsat, ale také ověřit jeho požadované vlastnosti. Obecně formální metody nedosáhly masivního nasazení kvůli časové náročnosti a zbytečně vysokému usilí. Hlavní doménou pro využití se staly systémy vyžadující bezchybný chod v kritických situacích (řízení leteckých systémů, lékařský software apod.). 

Formální specifikaci můžeme rozdělit na 2 typy:

  1. Specifikace chování (funkční
  2. Specifikaci vlastností systému (deskriptivní )

Specifikace chování

Jeden z nejznámějších přístupů k popisu chování systémů a tedy i nástrojů funkční specifikace jsou tzv. konečné automaty. Softwaroví inženýři dostávají k dispozici formální aparát umožňující jednoznačně definovat chování objektů a ověřovat tak jeho požadované dynamické vlastnosti.

Graficky lze vyjádřit konečný automat pomocí grafu, kde uzly grafu vyjadřují stavy systému a hrany označené vstupem definují přechody mezi těmito stavy. V jazyce UML je tato specifikace realizována pomocí stavových diagramů, kdy ověřujeme zda-li posloupnost zpráv přijatých objektem vede k dosažení jeho koncového stavu.

Příklad:

Specifikace vlastností systému

Nejčastěji používanou metodu specifikace vlastností systému je algebraická specifikace - používá k popisu 2 základní pojmy – druhy a operace. Druhy a operace jsou analogií k pojmům datové typy a procedury bežně používaných v programovacích jazycích. V případě algebraických specifikací operace odpovídá matematickému pojmu funkce, která zobrazuje n-tici hodnot na hodnotu. Druhy rozumíme neprázdné množiny hodnot reprezentující definiční obor
a obor hodnot funkcí (operací).

Strukura algebraické specifikace má následující formu:

Je tvořena 4 základními komponentami:
1. představení definuje druh (jméno typu) a deklaruje další používané algebraické specifikace,
2. popis neformálně popisuje operace a druh,
3. signatury definují syntaxi operací a jejich parametry,
4. axiomy (platná tvrzení) určují sémantiku operací cestou charakterizace jejich chování.

Příklad: Algebraická specifikace abstraktního datového typu Seznam. Seznam je tvořen elementy, které jsou přidávány na jeho konec a odebírány z jeho začátku.

  Zdroj skripta - Metody specifikace softwarových systémů (Prof.Ing. Ivo Vondrák CSc.)

Kam dál?