Kursa kods DatZ7026
Fakultāte Datorikas fakultāte
Kredītpunkti, lekciju skaits
Kredītpunkti ECTS kredītpunkti Kopējais auditoriju stundu skaits Lekciju stundu skaits Semināru un praktisko darbu stundu skaits Studenta patstāvīgā darba stundu skaits
4 6 64 32 32 96
E-kursi 2DAT7044: Specifikāciju valodas
Kursa anotācija Kurss padziļināti aplūko formālo specifikāciju veidošanā izmantotos matemātiskos formālismus, ietverot ASM, B, CASL, Café OBJ, DC, RAISE, VDM, TLA+ un Z, kā arī datorasistētu specifikāciju korektības pierādījumu veidošanas principus uz COQ un ISABELLE/HOL sistēmu bāzes.
Kursa atbildīgais Jānis Visvaldis Bārzdiņš
Rezultāti 1. Students pārzina matemātiskās struktūras un teorijas, kas ir formālo specifikāciju valodu pamatā (koncepti em12).

2. Students prot izmantot datorasistētas pierādījuma veidošanas sistēmas (analīze em21, realizācija em33).
Kursa plāns 1. Specifikāciju valoda Z
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
2. Specifikāciju valoda B
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
3. Specifikāciju valoda VDM
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
4. Specifikāciju valoda ASM
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
5. Specifikāciju valoda TLA+
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
6. Specifikāciju valoda un sistēma Café OBJ
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
7. Specifikāciju valoda CASL
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
8. Specifikāciju valoda DC
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
9. Specifikāciju valoda RAISE
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
10. Pierādījuma atbalsta sistēma COQ
Lekcija 3st, Seminārs 3st, Patstāvīgs darbs 9st.
11. Pierādījuma atbalsta sistēma ISABELLE/HOL
Lekcija 2st, Seminārs 2st,
Patstāvīgs darbs 6st.
Prasības kredītpunktu iegūšanai 1. Lekciju un semināru apmeklējums un aktīva dalība tajos (30%).
2. Referāti par kursā iekļautām specifikāciju valodām (30%).
3. Datorasistēta pierādījuma izveidošana (30%).
4. Mutisks eksāmens (10%).

Jāaizpilda LUIS anketa ar kursa novērtējumu (0%).
Mācību literatūra 1. D.Bjorner, M.Henson (eds.), Logics of Specification Languages. Springer, 2008. (LU bibliotēkā 1 eksemplārā)
2. Y.Bertot, P.Casteran, Interactive Theorem Proving and Program Development. Springer, 2004. (LU bibliotēkā 1 eksemplārā)

3. T.Nipkow, L.Paulsson, M.Wenzel, Isabelle/HOL; A Proof Assistant for Higher Order Logic. Springer, 2002. (LU bibliotēkā 1 eksemplārā)
Papildus literatūra 1. E.Boerger, R.Staerk, Abstract State Machines. Springer, 2003.
2. J.B.Wordsworth. Software Development with Z. Addison-Wesley, 1992.
3. J.B.Wordsworth. Software Engineering with B. Addison-Wesley, 1996.
4. C.B.Jones. Systematic Software Development using VDM. Prentice Hall, 1990.

5. J.Fitzgerald, P.G.Larsen, P.Mukherjee, N.Plat, M.Verhoef. Validated designs of object oriented systems. Springer, 2005
Studiju programmas Datorzinātnes