Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat
FIŞA DISCIPLINEI

Codul	Disciplina	
MI253	Metode formale în programare	

Specializarea	Semestrul	Ore: C+S+L	Categoria	Statutul	
Programare bazată pe componente - în limba engleză	1	2+2+0		obligatorie	
Metode formale în programare - în limba engleză	1	2+2+1		obligatorie	

Titularii de disciplină	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 analiza corectitudinea algoritmilor si sa masoare calitatile unui program.	
Conţinutul	1. Ce sunt metodele formale? Mituri. Aplicatii.
2. Specificare Formala:
  - necesitatea specificarii formale;
  - metode de specificare;
  - limbaje de specificare (Z, OBJ, VDM, ...);
  - necontradictia specificatiilor
3. Demonstrarea corectitudinii programelor
  - metode de demonstrare a corectitudinii;
  - automatizarea procesului verificarii;
4. Dezvoltarea programelor din specificatii
  - metode de dezvoltare;
5. Verificarea modelelor
6. Dezvoltarea orientata pe obiecte.	
Bibliografie	1. EHRIG H., B.Mahr, Fundamentals of Algebraic Specification, Springer-Verlag, 1985
2. FENTON N.E., Software Metrics. A Rigorous Approach, International Thomson Computer Press, 1995, 332 pages.
3. GOLDSACK S.J., S.J.H.KENT, Formal Methods and Object Technology, Springer-Verlag, 1986.
4. LANO K., Formal Object-Oriented Development, Springer-Verlag, 1995.
5. MORGAN C., Programming from Specifications, Prentice Hall, 1990.
6. SHERRELL L.B., D.L.CARVER, FunZ: An intermediate specification language, Computer Journal, 38(1995), 3, 193-207.
7. WOODCOCK,J., J. DAVIES, Uzing Z. Specification, Refinement and Proof, Prentice-Hall, 1996.
8. KIM S.D., Formal Specification in OO Software Development, PhD Thesis, 1991, Iowa University
9. *** Articole din Internet	
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.
Detalii la: www.cs.ubbcluj.ro/~mfrentiu/Lectures/