Fisa disciplinei MI018

Universitatea "Babeş-Bolyai" din Cluj-Napoca

Facultatea de Matematică şi Informatică
FISA DISCIPLINEI

Verificarea corectitudinii programelor Program correctness

Cod Semes-
trul Ore: C+S+L Credite Tipul Sectia

MI018 4 2+1+0 5 optionala Tehnologie Informatică
(College of Computer Technology)

MI018 6 2+1+0 5 optionala Informatică
(Computer Science)

Cadre didactice indrumatoare Teaching Staff in Charge

Prof. Dr. FRENŢIU Militon, mfrentiu@cs.ubbcluj.ro

Obiective Aims

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 programelor;
4. Formarea deprinderilor de proiectare a programelor corecte din specificatii;
5. Formarea unui stil modern de programare.
To understand what a correct algorithm is. To gain knowledge of designing correct algorithms and proving their correctness hand- in-hand. To learn the methods of testing and verifying programs. To become used with building correct programs from specifications. To acquire a modern programming style.

Continut

1. Logica pentru proiectarea programelor.
2. Specificarea programelor.
3. Partial-corectitudine, terminare, total corectitudine.
4. Metoda lui Floyd de demonstrare a corectitudinii.
5. Axiomatizarea lui Hoare.
6. Dijkstra: cea mai slaba preconditie.
7. Impactul teoriei corectitudinii programelor asupra programarii. Dezvoltarea corecta a programelor din specificatii.
8. Inspectarea programelor.
9. Testarea programelor.
10. Executie simbolica
11. Verificarea programelor.
12. Concluzii. Reguli de programare.

Bibliografie

1. Balanescu T., Corectitudinea programelor, Editura tehnica, Bucuresti 1995.
2. Dromey G., Program Derivation. The Development of Programs From Specifications, Addison Wesley Publishing Company, 1989.
3. Gries, The Science of Programming, Springer-Verlag, Berlin, 1981.
4. Manna, Z., Mathematical Theory of Computation, McGrawHill, NewYork, 1974.
5. Budd T.A., D.Anghin, Two Notions of Correctness and their Relation to Testing, Acta Informatica, 18(1982), 1, 31-46.
6. Correll C.H., Proving Programs Correct through Refinement, Acta Informatica, 9(1978), 121-132.

Evaluare Assessment

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 si cum a reusit sa-l prezinte in fata colegilor. La sfarsitul anului activitatea se incheie cu un colocviu. Acesta consta dintr-o discutie pe marginea cunostintelor predate la curs, cu accent pe intelegerea celor predate. In urma acestei discutii se va acorda o a doua nota. Nota finala va fi media aritmetica a celor doua note mentionate mai sus.
Each student must read a published research paper and present it at a seminary. He will obtain a mark for the presentation given to the seminary and for the way he expressed the ideas. The exam will consist of a talk based on which the student will obtain a second mark. The final mark will be the average of these two marks.