The subject of Programming Methodology introduces the student to the field of formal software development. In this subject, which is taught after Basic Programming, the basic concepts necessary to create and execute computer programs will be introduced, emphasizing formal specification methods.

- Capacity to analyse, design, construct and maintain applications in a robust and secure manner

- Capacity to specify, document, validate and verify programs

- Capacity to reason and justify properties related to programs

- Capacity to evaluate and compare specifications and documentation of programs from the quality point of view

- Knowledge of formal specification and program design methods

- Knowledge of basic notions of axiomatic semantics of programming languages

- Knowledge and application of basic algorithmic procedures of IT technologies for the design of solutions to problems, analysing the suitability and complexity of the algorithms proposed



Specific objectives:

- Specification, correction and design by contract

- Formal pre-post specification

- Hoare's formal system

- The equational specification technique

- The formal derivation method

- Topic 0: Introduction

- Topic 1: Logical Asertions

- Topic 2: Specification

- Topic 3: Verification

- Topic 4: Derivation

In the lectures there will be sessions of concepts exposition, reinforced with examples of situations in which these concepts are to be used.



In the practical part a set of exercises will be developed. The exercises to be carried out pose programming problems that students must perform in the most autonomous way as possible.



During the lectures group work will be carried out systematically, discussing and presenting the results of exercises with the aim of encouraging direct participation in the course and also students' motivation.

• Continuous Assessment System
• Final Assessment System
• Tools and qualification percentages:
  • Written test to be taken (%): 100

Assessment of the subject in the ordinary call is either done through continuous assessment or final assessment. By default, all students will do continuous assessment, unless they withdraw from it.



* Evaluation with final exam

It is allowed to withdraw from continuous assessment to take a single final exam. This withdrawal must be communicated the professor responsible for the course in the period set out in Article 8 of the Rules for Student Assessment. Withdrawals from continuous assessment will not be accepted after the dates stated, except in exceptional cases.



The exam will test the entire content of the subject. To pass the subject, it is necessary to obtain a minimum mark of 5 out of 10 in the exam.



* Continuous assessment

By default, continuous assessment is the standard method, unless the student has expressly withdrawn from it.



Continuous assessment is done through written tests to demonstrate that knowledge and competences taught in the subject have been acquired.



1) First-order logic (20% of the grade)

2) Sequences and conditionals (20% of the grade)

3) Iterations (30% of the grade)

4) Recursiveness and function calls (30% of the grade)



* Requirements to pass the ordinary call through continuous evaluation without final exam

- Perform all written tests

- Minimum score of 5 in the sum of all the tests

- Minimum score of 25% on each of the tests



* Ordinary final exam:

The only students who can present themselves are those who have passed at least three written tests, although they may not have reached the level required to pass an ordinary call in continuous assessment.



The exam will be divided into four parts, corresponding to each test:

The student may take the parts he/she wishes

The grades from previous tests will be maintained if they are not taken in this exam

The grade of previously taken tests will not be maintained (corresponding to the parts taken in this exam) for the purposes of the calculation of the final grade



* Requirements to pass the ordinary call:

- Have taken all the written tests (in the ordinary final exam or before)

- Minimum mark of 5 in the sum of all the written tests

- Minimum mark of 25% in each written test



* Withdrawal from the exam:

Students following continuous assessment may withdraw from the call as per that stated in Article 12 of the Rules for Student Assessment



* Cases of copying:

Article 11 of the Rules for Student Assessment will be applied.



* Continuous assessment

By default, continuous assessment is the standard method, unless the student has expressly withdrawn from it.

Continuous assessment is done through written tests, in which students must demonstrate that they have acquired the knowledge and competences taught in the subject.

1) First-order logic (20% of the grade)

2) Sequences and conditionals (20% of the grade)

3) Iterations (30% of the grade)

4) Recursiveness and function calls (30% of the grade)



* Requirements to pass the ordinary call through continuous evaluation without final exam

- Perform all written tests

- Minimum score of 5 in the sum of all the tests

- Minimum score of 25% on each of the tests



* Ordinary final exam:

The only students who can present themselves are those who have passed at least three written tests, although they may not have reached the level required to pass an ordinary call in continuous assessment.



The exam will be divided into four parts, corresponding to each test:

The student may take the parts he/she wishes

The grades from previous tests will be maintained if they are not taken in this exam

The grade of previously taken tests will not be maintained (corresponding to the parts taken in this exam) for the purposes of the calculation of the final grade



* Requirements to pass the ordinary call:

Have taken all the written tests (in the ordinary final exam or before)

Minimum mark of 5 in the sum of all the written tests

Minimum mark of 25% in each written test



* Withdrawal from the exam:

Students following continuous assessment may withdraw from the call as per that stated in Article 12 of the Rules for Student Assessment



* Cases of copying:

Article 11 of the Rules for Student Assessment will be applied.



* If the course cannot be assessed face-to-face, the relevant changes will be made to carry it out online by using the IT tools available at the UPV/EHU. The particulars of this online assessment will be made public.

The extraordinary call consists of an exam on 10 points in which the whole of the subject is evaluated.



To pass the subject, it is necessary to obtain a minimum score of 5 points out of the total of 10 exam points.



To waive the right to the examination, it will be sufficient not to appear. In this case, the qualification will be "No Presented".



* Note that no grade from the ordinary call is kept



* Cases of copying

Article 11 of the Rules for Student Assessment will be applied.



* If the course cannot be assessed face-to-face, the relevant changes will be made to carry it out online by using the IT tools available at the UPV/EHU. The particulars of this online assessment will be made public.

- Material of the subject (Notes and Laboratories)
- eGela virtual platform of the UPV/EHU for this subject

Basic bibliography

- Especificación, Verificación y Derivación Formal de Programas. J. Álvez, X. Arregi, J. Gaintzarain, P. Lucio y M. Marichalar, Pearson, 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