"Babes-Bolyai" University of Cluj-Napoca Faculty of Mathematics and Computer Science

 Program correctness
 Code Semes-ter Hours: C+S+L Credits Type Section MI018 6 2+1+0 5 optional Informatică MI018 6 2+1+0 4 optional Matematică-Informatică
 Teaching Staff in Charge
 Prof. FRENTIU Militon, Ph.D., mfrentiu@cs.ubbcluj.ro
 Aims 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.
 Content 1. Logic for proiectarea program design. 2. Program Specification. 3. Concepts: partial-correctness, termination, total correctness. 4. Floyd's method for proving program correctness. 5. Hoare's Axiomatization. 6. Dijkstra: the weakest precondition. 7. Stepwise refinement from specifications 8. Verification and validation: - program inspection;] - symbolic execution; - testing and debugging; - documentation. 9. Consequences on programming activity. Programming rules.
 References 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. M.Frentiu, Verificarea corectitudinii programelor, Ed.Univ."Petru-Maior", 2001. 4. Gries, The Science of Programming, Springer-Verlag, Berlin, 1981. 5. Manna, Z., Mathematical Theory of Computation, McGrawHill, NewYork, 1974. 6. Articole de specialitate (din Journale si Internet)
 Assessment 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 (mark R). The activity ends with a written examination (mark E). The final mark is the average of R and E, i.e. F=(R+E)/2