Metode formale în programare |
trul |
|||||
Cadre didactice indrumatoare |
Prof. Dr. FRENTIU Militon, mfrentiu@cs.ubbcluj.ro |
Obiective |
Sa predea studentilor tehnicile formale necesare in dezvoltarea sistemelor. Sa formeze deprinderi teoretice si practice de gandire matematica formala in specificarea, verificarea si dezvoltarea programelor. Sa fie capabili sa faca o analiza formala si sa analizeze fiecare etapa din dezvoltarea programelor. Sa poata evalua complexitatea algoritmilor si sa masoare calitatile unui program. |
Continut |
1. Specificare Formala:
- necesitatea specificarii formale; - metode de specificare; - limbaje de specificare (Z, OBJ, VDM, ...); - necontradictia specificatiilor 2. Demonstrarea corectitudinii programelor - metode de demonstrare a corectitudinii; - automatizarea procesului verificarii; 3. Dezvoltarea programelor din specificatii - metode de dezvoltare; 4. Dezvoltarea orientata pe obiecte |
Bibliografie |
1. Ehrig H., B.Mahr, Fundamentals of Algebraic Specification, Springer-Verlag, 1985
2. Goldsack S.J., and S.J.H.Kent, Formal Methods and Object Technology, Springer. 4. Lano K., Formal Object-Oriented Development, Springer 5. Morgan C., Programming from Specifications, Prentice Hall, 1990. 6. Sherrell L.B. and D.L.Carver, FunZ: An intermediate specification language, Computer Journal, 38(1995), 3, 193-207. 7. Jim Woodcock, Jim Davies, Uzing Z. Specification, Refinement and Proof, Oxford Univ. 8. Soo Dong Kim, Formal Specification in OO Software Development, PhD Thesis, 1991, Iowa University |
Evaluare |
O nota se da pentru o lucrare scrisa in ziua examenului si alta pentru activitate depusa in timpul anului. Rezultatul final va fi media aritmetica a celor doua note. |