Seminář z formálních specifikací

Garant předmětu:

Karel Richta

Přednášející:

Cvičící:

Karel Richta

Předmět zajišťuje:

katedra softwarového inženýrství

Anotace:

Student se naučí vyhodnocovat výhody a nevýhody použití formálních specifikací, pracovat s nástroji, které umí formální specifikace zpracovat a případně je využívat při vytváření či ověřování prototypů.

Požadavky:

Základy matematiky a logiky.

Osnova přednášek:

1. Syntaxe a sémantika specifikačních jazyků, různé způsoby specifikace systémů.

2. Algebraické specifikace, různé způsoby implementace algebraických specifikací.

3. Přepisovací systémy, převod specifikace na přepisovací systém.

4. Abstraktní přepisovací stroje, prototypování algebraických specifikací.

5. Příklady na prototypování specifikací.

Osnova cvičení:

Předmět probíhá formou semináře.

Cíle studia:

Naučit studenty pracovat s formálními specifikacemi, využívat je při dokumentaci a při návrhu systémů.

Studijní materiály:

1. Bjorner, Henson: Logics of Specification Languages. Springer, ISBN 978-3-540-74106-0, 2008.

2. Richta, Velebil: Sémantika programovacích jazyků. Skripta UK, 1997.

3. Goguen, Winkler, Meseguer, Futatsugi, Jouannaud: Introducing OBJ. SRI-CSL-92-03, Menlo Park 1992.

4. Watt: Programming Language Syntax and Semantics, Prentice Hall 1991.

5. McCombs: Maude 2.0 Primer. http://maude.cs.uiuc.edu/primer/maude-primer.pdf, 2003.

Poznámka:

Rozvrh na zimní semestr 2024/2025:

Rozvrh není připraven

Rozvrh na letní semestr 2024/2025:

Rozvrh není připraven

Předmět je součástí následujících studijních plánů:

• Informatika (doktorská) (povinně volitelný předmět)
• Informatika (povinně volitelný předmět)