Publikace na Matematicko-fyzikální fakulta |
2009
Abstrakt
Ověřování modelu softwaru je typicky aplikováno na komponenty velkých systémů. Generování předpokladů spočívá v hledání co nejméně omezujícího prostředí, v němž bude softwarová komponenta splňovat danou podmínku.
Dříve byl popsán algoritmus, který toto prostředí určí pro případ regulárních jazyků. V tomto článku navrhujeme obecné schéma pro výpočet předpokladů i pro neregulární vlastnosti a ukazujeme jednoznačnost nejméně omezujícího prostředí pro libovolnou třídu jazyků.
Obecně můžeme v případě neregulárních jazyků narazit na algoritmickou nerozhodnutelnost. Ukazujeme též metodu pro výpočet předpokladů založenou na visibly pushdown automatech a jejich abstrakcích s konečným počtem stavů.