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

Formal methods in programming
Code
Semes-
ter
Hours: C+S+L
Credits
Type
Section
MI253
1
2+2+0
9
compulsory
Programare bazată pe componente - în limba engleză
MI253
1
2+2+1
9
compulsory
Metode formale în programare - în limba engleză
Teaching Staff in Charge
Prof. FRENTIU Militon, Ph.D.,  mfrentiucs.ubbcluj.ro
Aims
To introduce the students to the formal techniques needed in the development of systems. To have an understanding of both the theory and practice of formal mathematical thinking in software specification, verification and development. To be able to perform formal analysis and to reason about designs and developments. To obtain the ability to analyse the correctness of algorithms, and to measure the qualities of programs.
Content
1. What are Formal Methods? Myths. Applications.
2. Formal Specification:
- the necessity of formal specifications;
- specification methods;
- specification languages (Z, OBJ, VDM, ...);
- necontradictia specificatiilor
3. The proof of program correctness:
- methods for proving correctness;
- automatizing verification process.
4. Refinement of programs from specifications:
5. Object Oriented Development.
References
1. EHRIG H., B.Mahr, Fundamentals of Algebraic Specification, Springer-Verlag, 1985
2. FENTON N.E., Software Metrics. A Rigorous Approach, International Thomson Computer Press, 1995, 332 pages.
3. GOLDSACK S.J., S.J.H.KENT, Formal Methods and Object Technology, Springer-Verlag, 1986.
4. LANO K., Formal Object-Oriented Development, Springer-Verlag, 1995.
5. MORGAN C., Programming from Specifications, Prentice Hall, 1990.
6. SHERRELL L.B., D.L.CARVER, FunZ: An intermediate specification language, Computer Journal, 38(1995), 3, 193-207.
7. VADERA S., F.MEZIANE, From English to Formal Specifications, Computer Journal, 37(1994), 9, 753-763.
8. WOODCOCK,J., J. DAVIES, Uzing Z. Specification, Refinement and Proof, Prentice-Hall, 1996.
8. KIM S.D., Formal Specification in OO Software Development, PhD Thesis, 1991, Iowa University
Assessment
A first grade will be given for a final written examination covering both theory and practice, and a second grade will be given for the activity during the term. The final result will be the average of these two grades.