Uživatelem řízené proveditelné specifikace

Jedna z nedostatků klasických metod pro specifikaci softwarových požadavků je obtížnost ověření konzistence a adekvátnosti specifikací. Softwarové inženýrství reagovalo na tuto skutečnost různými metodami (např. model based software engineering, agile software development, executable algebraic specification), které dovolují vidět praktické chování specifikací co nejdřív ve vývojovém procesu. Tyto metody ale dělají kompromisy ohledně jiných aspektů např. týkající se expresivity anebo preciznosti. V rámci tohoto tématu student navrhne formální jazyk, který splní dva na první pohled protichůdné cíle: Klíč pro současné splnění obou cílí budou anotace, kterými uživatel jazyku poskytuje informaci o exekuci specifikace tak, aby zvýšená snaha o psaní anotací měla za důsledek zvýšenou účinnost exekuce. První krok bude vývoj nástroje pro výuku, který dovoluje studentům, kteří píšou specifikace jako úkol ve cvičeni, jejich řešení hned i spustit i otestovat.