Wirsing, P.: Algebraic Specifications. Handbook of Theoretical Computer Science, Vol. B, Formal Models and Semantics, Elsevier Science Publisher B.V., 1990
Van Horebeek,I., Lewi,J.: Algebraic Specifications in Software Engineering. Springer Verlag, 1989
Potter,B., Sinclair,J., Till,D.: An Introduction to Formal Specifications and Z. Prentice Hall, 1991
Wordsworth,J.B.: Software Development with Z (A Practical Approach to Formal Methods of Software Engineering). Addison Wesley, 1992
Alagar,V.S., Periyasamy,K.: Specification of Software Systems. Springer Verlag, 1998
2-INF-127 Formálne špecifikácie
| Odporúčaný ročník: | 1. |
| Semester: | letný |
| Rozsah: | P4 |
| Hodnotenie: | 0/100 |
| Počet kreditov: | 6 |
| Vyučujúci: | prednáša RNDr. Igor Prívara CSc. |
| www stránka: |
Cieľ:
- zdôrazniť úlohu formálnych metód vo vývoji programov
- prezentovať dva základné prístupy k formalizácii špecifikácii založené na špecifikácií vlastnosti (algebraické špecifikácie), resp. na špecifikácii modelu (Z-špecifikácie)
- pri oboch špecifikačných metódach študovať otázky
- modulárneho návrhu už na úrovni špecifikácií
- sémantiky (modelov) špecifikácie
- dokazovania vlastností špecifikácie
- postupného zjemňovania (implementácie) špecifikácie
- prototypizácie špecifikácie
- ilustrovať obe špecifikačné metódy na príkladoch rôzneho rozsahu
Sylabus:
- formálne špecifikácie - ich postavenie vo vývoji programov a požiadavky na metódy formalizácie, stručné zhrnutie a porovnanie rôznych prístupov
- algebraická špecifikácia - signatúra a axiómy, algebraická špecifikácia v jazyku SL, modulárny návrh algebraickej špecifikácie (skladanie špecifikácií, parametrické špecifikácie), špecifikácia výnimočných a chybových stavov
- sémantika algebraickej špecifikácie - modely algebraickej špecifikácie, rôzne prístupy charakterizácie sémantiky algebraickej špecifikácie (iniciálna, voľná a behaviorálna sémantika), sémantické požiadavky pri skladaní špecifikácií (dostatočná úplnosť a konzistentnosť), hierarchická sémantika algebraickej špecifikácie
- konštruktívne algebraické špecifikácie - konštruktory, induktívny návrh axióm (pravidiel), výpočtový model algebraických špecifikácií (prepisovacie systémy), kanonická špecifikácia
- implementácia špecifikácie - implementácia resp. behaviorálna implementácia špecifikácie
- ekvacionálna logika - ekvacionálne dokazovania v jednodruhovom, mnohodruhovom a druhovo usporiadanom prostredí, dokazovanie v induktívnych teóriách, dokazovanie behaviorálnych vlastností
- Z-špecifikácie - preddefinovane typy v špecifikačnom jazyku Z (množiny, typy, logické funkcie a kvantifikátory, relácie a funkcie), špecifikačné schémy (skladanie špecifikácií, generické špecifikácie)
- postupné zjemnenie Z-špecifikácií, vývoj programu zo špecifikácií, princípy návrhu dátových štruktúr a algoritmov pomocou Z
- porovnávacia štúdia - algebraické špecifikácie vs. Z-špecifikácie
Literatúra: