Formální metody vývoje softwaru

Formal methods

Matematicky založené techniky pro přesné specifikování a ověřování vlastností systému.

Formální metody popisují požadavky, návrh nebo chování softwaru pomocí přesných matematických modelů a logiky. Umožňují dokazovat vybrané vlastnosti, například že určitý stav není dosažitelný nebo že operace zachovává invariant. Jejich použití může odhalit chyby už před spuštěním systému, vyžaduje však odborné znalosti a pečlivé vymezení toho, co důkaz skutečně pokrývá.