Program correctness |
ter |
|||||
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 |