Disciplina: Metode formale în programare	Cod: MI253	

Semestrul	Ore: C+S+L	Tipul	Specializarea	
1	2+2+0	obligatorie	Programare bazata pe componente - în limba engleza	
1	2+2+1	obligatorie	Metode formale în programare - în limba engleza	

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 analiza corectitudinea algoritmilor si sa masoare calitatile unui program	
Continut	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. Dezvoltarea orientata pe obiecte	
Bibliografie selectiva	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 Interne	
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