Universitatea "Babeş-Bolyai" din Cluj-Napoca

Facultatea de Matematică şi Informatică
FISA DISCIPLINEI

Metode formale în programare

Formal methods in programming

Cod	Semes- trul	Ore: C+S+L	Credite	Tipul	Sectia
MI253	2	2+2+0	9	obligatorie	Programare bazată pe componente - în limba engleză (Component-Based Programming - in English)

Cadre didactice indrumatoare

Teaching Staff in Charge

Prof. Dr. FRENŢIU Militon, mfrentiu@cs.ubbcluj.ro

Obiective

Aims

Sa predea studentilor tehnicile formale necesare in dezvoltarea sistemelor. Sa formeze deprinderi teoretice si practice de gandire matematica formala in specificarea, verificarea si dezvoltarea programelor. Sa fie capabili sa faca o analiza formala si sa analizeze fiecare etapa din dezvoltarea programelor. Sa poata evalua complexitatea algoritmilor si sa masoare calitatile unui program.

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 evaluate the complexity of specific algorithms, and to measure the qualities of programs.

Continut

1. Specificare Formala: - necesitatea specificarii formale; - metode de specificare; - limbaje de specificare (Z, OBJ, VDM, ...); - necontradictia specificatiilor 2. Demonstrarea corectitudinii programelor - metode de demonstrare a corectitudinii; - automatizarea procesului verificarii; 3. Dezvoltarea programelor din specificatii - metode de dezvoltare; 4. Dezvoltarea orientata pe obiecte

Bibliografie

1. Ehrig H., B.Mahr, Fundamentals of Algebraic Specification, Springer-Verlag, 1985 2. Goldsack S.J., and S.J.H.Kent, Formal Methods and Object Technology, Springer. 4. Lano K., Formal Object-Oriented Development, Springer 5. Morgan C., Programming from Specifications, Prentice Hall, 1990. 6. Sherrell L.B. and D.L.Carver, FunZ: An intermediate specification language, Computer Journal, 38(1995), 3, 193-207. 7. Jim Woodcock, Jim Davies, Uzing Z. Specification, Refinement and Proof, Oxford Univ. 8. Soo Dong Kim, Formal Specification in OO Software Development, PhD Thesis, 1991, Iowa University

Evaluare	Assessment
O nota se da pentru o lucrare scrisa in ziua examenului si alta pentru activitate depusa in timpul anului. Rezultatul final va fi media aritmetica a celor doua note.	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.