- Capacidad para analizar, diseñar, construir y mantener aplicaciones de forma robusta y segura

- Capacidad para especificar, documentar, validar y verificar programas

- Capacidad para razonar y justificar propiedades relativas a programas

- Capacidad para valorar y comparar especificaciones y documentación de programas desde el punto de vista de la calidad

- Conocimiento de métodos formales de especificación y diseño de programas

- Conocimiento de las nociones básicas en semántica axiomática de lenguajes de programación

- Conocimiento y aplicación de los procedimientos algorítmicos básicos de las tecnologías informáticas para diseñar soluciones a problemas, analizando la idoneidad y complejidad de los algoritmos propuestos



Objetivos específicos:

- Especificación, corrección y diseño por contrato

- Especificación formal pre-post

- El sistema formal de Hoare

- La técnica de especificación ecuacional

- El método de derivación formal

Tema 0: Introducción

Tema 1: Aserciones Lógicas

Tema 2: Especificación

Tema 3: Verificación

Tema 4: Derivación

En las clases magistrales se realizarán sesiones de exposición de conceptos, reforzados con ejemplos de situaciones en que dichos conceptos se han de emplear.



En las clases de ejercicios se desarrollarán un conjunto de ejercicios. Los ejercicios a realizar plantean problemas informáticos que los alumnos deberán realizar de la forma más autónoma posible.



Durante el desarrollo de las clases se llevarán a cabo, de forma sistemática, actividades de trabajo en grupo, discusión y presentación de resultados de ejercicios, con el fin de impulsar la participación directa en el desarrollo del curso y de fomentar la motivación del alumnado.

La evaluación de la asignatura en la convocatoria ordinaria se realiza mediante evaluación continua o evaluación final. La opción por defecto es la evaluación continua salvo que se renuncie a ella.



* Evaluación mediante prueba final:

Se permite renunciar a la evaluación continua para realizar la evaluación final. Esta renuncia se deberá comunicar al profesorado responsable en los plazos estipulados en el Artículo 8 de la normativa sobre la evaluación del alumnado. No se aceptarán renuncias a la evaluación continua posteriores a las fechas habilitadas para ello salvo casos excepcionales.



El examen evaluará todo el conjunto de la asignatura. Para aprobar la asignatura, es necesario obtener una calificación mínima de 5 puntos sobre el total de 10 puntos del examen.



* Evaluación continua:

La evaluación por defecto de la asignatura se hace mediante evaluación continua, salvo que se haya renunciado expresamente a ella.



La evaluación continua se realiza mediante pruebas escritas para demostrar que se han adquirido los conocimientos y las competencias impartidas en la asignatura.



Pruebas escritas:

1) Lógica de Primer Orden (20% de la nota)

2) Secuencias y condicionales (20% de la nota)

3) Iteraciones (30% de la nota)

4) Recursividad y llamadas a funciones (30% de la nota)



Requisitos para aprobar la convocatoria ordinaria mediante evaluación continua sin examen final

- Realizar todas las pruebas escritas

- Nota mínima de 5 en la suma de todas las pruebas

- Nota mínima de 25% en cada una de las pruebas



* Examen final ordinario de la convocatoria ordinaria:



Podrán presentarse únicamente quienes, no habiendo alcanzado los requisitos para aprobar la convocatoria ordinaria mediante evaluación continua sin examen final, hayan realizado al menos tres pruebas escritas.



El examen se dividirá en cuatro partes correspondientes a cada prueba:

- Se podrán realizar las partes que se deseen

- Se mantendrán las notas de las pruebas anteriores cuyos partes no se realicen en este examen

- Se perderá la nota de las pruebas anteriormente realizadas, correspondientes a las partes que se realicen en este examen, a efectos del cálculo de la nota final



Requisitos para aprobar la convocatoria ordinaria:

- Haber realizado todas las pruebas escritas (en el examen final ordinario o anteriormente)

- Nota mínima de 5 en la suma de todas las pruebas escritas

- Nota mínima de 25% en cada prueba escrita



* Renuncia al derecho al examen:

El alumnado que sigue la evaluación continua podrá realizar la renuncia a la convocatoria de acuerdo con lo estipulado en el Artículo 12 de la normativa sobre la evaluación del alumnado.



El alumno que no se presente a dos o más pruebas escritas en la convocatoria ordinaria, obtendrá como calificación final "No Presentado", independientemente de que haya realizado, o no, el resto de pruebas escritas y/o actividades del curso.



* Casos de copia:

Se aplicará el Artículo 11 de la normativa vigente referente a la evaluación del alumnado.



Si no se puede realizar una evaluación presencial de la asignatura, se realizarán los cambios pertinentes para hacerlo online mediante la utilización de las herramientas informáticas existentes en la UPV/EHU. Las características de esta evaluación online serán hechas públicas.

- Material de la asignatura (Apuntes y Laboratorios)
- Plataforma Virtual eGela de la UPV/EHU para la asignatura "Metodología de la Programación"

Oinarrizko bibliografia

- 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.

Gehiago sakontzeko bibliografia

- 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.

Aldizkariak

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