Description of the subject:

One way to deal with program correction is by providing data to the program and analising wether the results are appropriate. Regarding program construction, one option is to base the design of programs on the non-formal knowledge of the designer, and then, to check the correctness of the program by using some data and, if necessary, to make amendments. Such an approach does not guarantee the correctness of the designed program. In the subject "Metodology of Programming" we will present formal methods to verify the correctness of programs and to build correct programs. These formal methods are based on mathematical logic. By using such methods, we can mathematically prove wether a program is correct or not, and we can mathematically design correct programs.



Context:

This subject is taught in the second semester of the first term. Previously, in the first semester, the basics of imperative programming have been presented in a non-formal way to the students. So the second semester is the right moment to introduce the students in the area of formal (mathematical) methods to deal with programming. This will provide them the necessary knowledge and skills to face, in an appropriate manner, the other subjects that will deepen in programming issues in the following semesters.

- Skills in analysis, design, implementation, and maintenance of correct software.

- Skills in program specification, documentation, validation, and verification.

- Skills to reason about program properties.

- To know the relationship between iteration and recursion.

- To know techniques for correct program transformation.

- To know basic notions about axiomatic semantics of programming languages.

1) Specification, correction and design by contract.

2) Preconditions and postconditions. Formal specification and formal documentation of programs.

3) Hoare's formal system: formal verification and formal derivation of programs.

4) Recursion.

5) Algebraic specification of abstract data types.

6) Transformation of recursive programs: transformation from recursive format to iterative format.

In the lectures, the theoretical contents will be presented together with relevant examples that ilustrate the application of the theory to real problems. Students will have to deal with exercices to master the presented techniques.



ONLINE TEACHING (EXCEPTIONAL SITUATIONS)

If face-to-face (or in-person) classes are not possible, the teaching activities and continuous evaluation activities will be reorganised and adapted to distance (or online) teaching. In order to achieve that goal, available resources will be used (eGela etc.). Students will be properly informed by means of eGela.

• Continuous Assessment System
• Final Assessment System
• Tools and qualification percentages:
  • Written test to be taken (%): 90
  • Realization of Practical Work (exercises, cases or problems) (%): 10

Two evaluation methods:

- Final evaluation: written examination about the whole subject at the end of the semester. Different exercices to work on the main contents of the subject. Only passed exercices will be taken into account to calculate the final punctuation.

- On-going (or continuous) evaluation: one written examination for each main content of the subject. The exams will be held along the semester. Passed exams will liberate the corresponding content and the punctuation will be summed to calculate the final punctuation. At the end of the semester, students that have not reached 5 points will have the opportunity to repeat the non-liberated exercices in order to try to reach to 5 points.



Changing from one evaluation method to the other: students can change from one evaluation methond to the other at any time before the day of the final examination (at the end of the semester).



Anyone that has not yet 5 points and does not take the final examination, will have a "not presented" as the final result.



CONTINUOUS EVALUATION (EXCEPTIONAL SITUATIONS)

If face-to-face (or in-person) continuous evaluation is not possible, the continuous evaluation

will be reorganised and adapted to distance (or online) continuous evaluation. In order to achieve

that goal, available resources will be used (eGela etc.). Students will be properly informed by means of eGela.



ONLINE EVALUATION (EXCEPTIONAL SITUATIONS)

If face-to-face (or in-person) evaluation is not possible, the evaluation will be realized online.

In order to achieve that goal, available resources will be used (eGela etc.). Students will be

properly informed by means of eGela.

Same approach as in ordinary evaluation.



ONLINE EVALUATION (EXCEPTIONAL SITUATIONS)

If face-to-face (or in-person) evaluation is not possible, the evaluation will be realized online.

In order to achieve that goal, available resources will be used (eGela etc.). Students will be

properly informed by means of eGela.

Material at eGela.

Basic bibliography

Especificación, Verificación y Derivación Formal de Programas. Javier Álvez, Xabier Arregi, Jose Gaintzarain, Paqui

Lucio, Montse Maritxalar. Pearson, 2015.



Programen Espezifikazio, Egiaztapen eta Eratorpen Formala. Javier Álvez, Xabier Arregi, Jose Gaintzarain, Paqui Lucio,

Montse Maritxalar. Udako Euskal Unibertsitatea (UEU), 2016.



Programen Egiaztapena eta Eratorpena. X. Arregi, A. Díaz de Ilaraza, P. Lucio. Udako euskal Unibersitatea, 1993.



Metodología y Tecnología de la Programación II. M. Díaz Roca,, J. C. Rodríguez del Pino. Univ. Palmas Gran Canaria, 2004.



Verificación de Programas y Metodología de la Programación. A. Díaz de Ilarraza, P. Lucio. Servicio Editorial Universidad del País Vasco, 1990.



Program Derivation. The Development of Programs from Specifications. G. Dromey. Addison-Wesley, 1989.

In-depth bibliography

Program Construction and Verification. R. C. Backhouse. Prentice-Hall, 1986.

Programación metódica. J.L. Balcázar. MacGraw-Hill, 1993.

Diseño de Programas.- Formalismo y Abstracción. Ricardo Peña. Prentice Hall, 1998.

Journals

Acta Informatica
Programming and Computer Software
Science of Computer Programming
Software Quality Journal
Transactions on Software Engineering and Methodology

Web addresses

http://www.sc.ehu.es/jiwlucap/metodologia.html

http://en.wikipedia.org/wiki/Formal_verification

http://en.wikipedia.org/wiki/Design_by_contract