Disciplina: Verificarea corectitudinii programelor	Cod: MI018	

Semestrul	Ore: C+S+L	Tipul	Specializarea	
6	2+1+0	optionala	Informatica	
6	2+1+0	optionala	Matematică-Informatică	

Cadre didactice indrumatoare	Prof. Dr. FRENTIU Militon, mfrentiu@cs.ubbcluj.ro	
Obiective	1. Intelegerea notiunilor de algoritm partial si total corect;
2. Formarea deprinderilor de proiectare a algoritmilor in paralel cu demonstrarea corectitudinii lor;
3. Insusirea metodelor de verificare si validare a programelor;
4. Formarea deprinderilor de proiectare a programelor corecte din specificatii;
5. Formarea unui stil modern de programare.	
Continut	I. Teoria corectitudinii programelor (4 cursuri)
 -  Specificarea programelor.
 - Metoda lui Floyd de demonstrare a corectitudinii.
 - Metoda lui Hoare de demonstrare. 
 - Axiome şi reguli pentru logica Floyd-Hoare: completitudine şi necontradicţie. 
 - Dezvoltarea corecta a programelor din specificaţii
 - Evoluţia istorică a corectitudinii programelor. Contribuţii: Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan
II. Verificarea şi validarea sistemelor  (3 cursuri)
 - conceptele verificare şi validare; asemănări şi deosebiri
 - metode de verificare
 - inspectarea programelor
 - necesitatea documentării programelor
 - execuţie simbolică
III. Testarea programelor. (3 cursuri)
 - conceptul de testare
 - tipuri de testare: a unei proceduri, a unui modul, T.de integrare,  T. de regresie, T. sistemului, T.de acceptare
 - criterii de testare
 - determinarea datelor de test
 - automatizarea testării
IV. Verificarea modelelor (model checking) (2 cursuri)
V. Legătura între diferitele metode de verificare (2 cursuri)
 - corectitudine-inspectare-testare-execuţie simbolică
 - Cleanroom. Program Quality
 - Impactul teoriei corectitudinii programelor asupra programarii. Reguli de programare.	
Bibliografie selectiva	1. BALANESCU T., Corectitudinea programelor, Editura tehnica, Bucuresti 1995.
2. DIJKSTRA, E., A constructive approach to the problem of program correctness, BIT, 8(1968), pg.174-186.
3. DIJKSTRA, E., Guarded commands, nondeterminacy and formal derivation of programs, CACM, 18(1975), 8, pg.453-457.
4. DROMEY G., Program Derivation. The Development of Programs From Specifications, Addison Wesley Publishing Company, 1989.
5. FRENTIU, M., Verificarea corectitudinii programelor, Ed.Univ."Petru-Maior", 2001.
6. GRIES, D., The Science of Programming, Springer-Verlag, Berlin, 1981.
7. HOARE, C.A.R., An axiomatic basis for computer programming, CACM, 12(1969), pg.576-580, 583.
8. MANNA, Z., Mathematical Theory of Computation, McGrawHill, NewYork, 1974.
9. M.Frentiu, H.F.Pop, Fundamentals of Programming, Babes-Bolyai Press, 200	
Evaluare	La seminar fiecare student va prezenta un referat pe care se va acorda o nota de apreciere a modului in care studentul a inteles articolul de specialitate citit, cum a reusit sa-l prezinte in fata colegilor si a discutiilor din cadrul seminariilor(nota R). La sfarsitul anului activitatea se incheie cu un examen (nota E). Media finala este media celor doua note mentionate, adica F=(R+E)/2