Universitatea Babeş-Bolyai Cluj-Napoca
Facultatea de Matematică şi Informatică
Ciclul de studii: Masterat
Domeniul: Informatica
Programul de studii: Programare bazată pe componente (în limba engleză)
Limba de predare: Engleză

SYLLABUS

I. General data
Code	Subject	
MI253	Formal Methods in Programming	

Semester	Hours: C+S+L	Category	Status	
1	2+2+0		compulsory	

II. Full status faculty members
Name and	Scientific	Didactic	Chair	Type of activity	
surname	title	title		C	S	L	
FRENTIU Militon	Ph.D.	Prof.	Programming  Languages and Methods	*			

Associated faculty members
Name and	Scientific	Institution	Type of	Type of activity	
surname	title		position	C	S	L	

III. Course objectives
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.	

IV. Course contents
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. Model Checking
6. Object Oriented Development.	

V. Bibliography
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. 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
9. *** Articole din Internet	

VI. Thematic of didactic activities per weeks

VII. Didactic methods used

VIII. 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.
Details at: www.cs.ubbcluj.ro/~mfrentiu/Lectures/	

IX. Additional references

	Dean,							Chair head,

	Date,							Course responsible,
								Prof. FRENTIU Militon, Ph.D.