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:
- Specifikace chování (funkční)
- 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.)