Universitatea "Babes-Bolyai" Cluj-Napoca
Facultatea de Matematica si Informatica
FISA DISCIPLINEI

Metode formale în programare
Cod
Semes-
trul
Ore: C+S+L
Credite
Tipul
Specializarea
MI253
1
2+2+0
9
obligatorie
Programare bazată pe componente - în limba engleză
MI253
1
2+2+1
9
obligatorie
Metode formale în programare - în limba engleză
Cadre didactice indrumatoare
Prof. Dr. FRENTIU Militon,  mfrentiucs.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
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. VADERA S., F.MEZIANE, From English to Formal Specifications, Computer Journal, 37(1994), 9, 753-763.
8. 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
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.