Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Licenţă
Domeniul: Informatică
Programul de studii: Informatică - linia de studiu română
Limba de predare: Română

SYLLABUS

I. Date generale
Codul	Disciplina	
MID0010	Verificarea şi validarea sistemelor soft	

Semestrul	Ore: C+S+L+P	Categoria	Statutul	
6	2+1+1+0	specialitate	obligatorie	

II. Cadre didactice cu norma de bază în Universitate
Numele şi	Titlul	Gradul	Catedra	Tipul activităţii	
prenumele	ştiinţific	didactic		C	S	L	
FRENTIU Militon	Dr. 	Prof.	Informatică	*			

Cadre didactice asociate
Numele şi	Titlul	Instituţia	Tipul	Tipul activităţii	
prenumele	ştiinţific		postului	C	S	L	

III. Obiectivele disciplinei
1. Intelegerea notiunilor de algoritm partial si total corect;
2. Formarea deprinderilor de proiectare a algoritmilor in paralel cu demonstrarea corectitudinii lor;
3. Cunoasterea metodelor de testare si verificare a sistemelor soft;
4. Formarea deprinderilor de proiectare a programelor corecte din specificatii;
5. Formarea unui stil modern de programare.	

IV. Conţinutul disciplinei
I. Teoria corectitudinii programelor (4 cursuri)
 -  Specificarea programelor.
 - Metoda lui Floyd de demonstrare a corectitudinii.
 - Metoda lui Hoare de demonstrare. 
 - Axiome si reguli pentru logica Floyd-Hoare: completitudine si necontradictie. 
 - Dezvoltarea corecta a programelor din specificatii
 - Evolutia istorica a corectitudinii programelor. Contributii: Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan
II. Verificarea si validarea sistemelor  (3 cursuri)
 - conceptele verificare si validare; asemanari si deosebiri
 - metode de verificare
 - inspectarea programelor
 - necesitatea documentarii programelor
 - executie simbolica
III. Testarea programelor. (2 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 testarii
IV. Verificarea modelelor (model checking) (2 cursuri)
V. Consecinte asupra metodologiei programarii (3 cursuri)
  - Cleanroom. 
  - SPI. SQA
  - Impactul teoriei corectitudinii programelor asupra programarii. Reguli de programare.	

V. Bibliografie
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 sistemelor soft, Ed. Presa Universitara Clujană, 2010.
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. Morgan, C., Programing from Specifications, Prentice Hall, NewYork, 1990.
B. Internet 	

VI. Tematica activităţilor didactice pe săptămâni
I. Teoria corectitudinii programelor (4 cursuri)
 -  Specificarea programelor.
 - Metoda lui Floyd de demonstrare a corectitudinii.
 - Metoda lui Hoare de demonstrare. 
 - Axiome si reguli pentru logica Floyd-Hoare: completitudine si necontradictie. 
 - Dezvoltarea corecta a programelor din specificatii
 - Evolutia istorica a corectitudinii programelor. Contributii: Floyd, Hoare, Dijkstra, Gries, Droomey, Morgan
II. Verificarea si validarea sistemelor  (3 cursuri)
 - conceptele verificare si validare; asemanari si deosebiri
 - metode de verificare
 - inspectarea programelor
 - necesitatea documentarii programelor
 - executie simbolica
III. Testarea programelor. (2cursuri)
 - 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 testarii
IV. Verificarea modelelor (model checking) (2 cursuri)
V. Consecinte asupra metodologiei programarii (2 cursuri)
  - Cleanroom. 
  - SPI. SQA
  - Impactul teoriei corectitudinii programelor asupra programarii. Reguli de programare.

VII. Metode didactice folosite
Expunere, conversaţie, studii de caz	

VIII. Evaluare
Activitatea la seminar, constand in participarea la discutii si rezolvarea unor probleme la tabla se noteaza prin nota A. Activitatea la laborator se noteaza prin L. La sfarsitul anului activitatea se incheie cu un examen scris, notat cu E. Nota finala F va fi media aritmetica a notelor mentionate mai sus: F=(A+L+2E)/4.
Details at: www.cs.ubbcluj.ro/~mfrentiu/Lectures/	

IX. Bibliografie suplimentară

	Decan,							Sef de catedra,

	Data,							Titular curs,
								Prof. Dr.  FRENTIU Militon