| Verificarea corectitudinii programelor | Program correctness |
trul |
|||||
(College of Computer Technology) |
|||||
(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. |
|
1. Logica pentru proiectarea programelor.
2. Specificarea programelor. 3. Corectitudinea schemelor logice: partial-corectitudine, terminare, total corectitudine. Metoda lui Floyd de demonstrare a corectitudinii. 4. Corectitudinea schemelor logice cu tablouri. 5. Corectitudinea programelor. Metoda lui Hoare de demonstrare. 6. Corectitudinea programelor recursive. 7. Testarea programelor. 8. Impactul teoriei corectitudinii programelor asupra programarii. Dezvoltarea corecta a programelor. 9. Verificarea programelor. 10. Sinteza programelor. 11. Reguli de programare. |
|
A. Carti:
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. B. Articole de specialitate: 1. T.A.Budd, D.Anghin, Two Notions of Correctness and their Relation to Testing, Acta Informatica, 18(1982), 1, 31-46. 2. C.H.Correll, Proving Programs Correct through Refinement, Acta Informatica, 9(1978), 121-132. 3. Dijkstra, A constructive approach to the problem of program correctness, BIT, 8(1968), pg.174-186. 4. Dijkstra, Guarded commands, nondeterminacy and formal derivation of programs, CACM, 18(1975), 8, pg.453-457. 5. G.Engels, U.Pletot, H.D.Elvich, An Operational Semantics for Specifications of ADTs with error Handling, Acta Informatica, 19(1983), 3, 235-254. 6. M.Foley, and C.A.R.Hoare, Proof of a recursive program: QUICKSORT, Computing Journal, 14(1971), 4, pg.391-395. 7. N.Francez, A.Pnueli, A Proof Method for cycling Programs, Acta Informatica, 9(1978), 133-157. 8. Geller M., Test data as an aid in proving programm correctness, CACM, 21(1978),5, 368-375. 9. Gelperin D. and B.Hetzel, The Growth of Software Testing, CACM, 31(1988), 6, 687-695. 10. R.Hamlet, Reliability Theory of Program Testing, Acta Informatica, 16(1981), 1, 31-44. 11. Hoare, An axiomatic basis for computer programming, CACM, 12(1969), pg.576-580, 583. 12. C.A.R.Hoare, Proof of a program:FIND, CACM, 14(1971), pg. 39-45. 13. Hogger, Derivation of Logic Programs, JACM, 20(1981), 2, pg.372-392. 14. Igarashi, London, and Luckham, Automatic Program Verification I: a logical basis and its implementation, Acta Informatica, 4(1975), 145-182. 15. Jacobs, and Gries, General correctness: a unification of partial and total correctness, Acta Informatica, 22(1985), 67-83. 16. Katz, and Manna, Logical analysis of programs, CACM, 19(1976), pg.188-206. 17. London, Proving Programs Correctness. Some Techniques and Examples, BIT, 10(1970), pg.168-182. 18. London, Proof of Algorithms. A new kind of certification, CACM, 13(1970), pg.371-373. 19. Wegbreit, The synthesis of loop predicates, CACM, 17(1974), 102-112. |
| 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. |