"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