DESCRIPCIÓN DE LA ASIGNATURA: Para decir si un programa es correcto, una opción es darle datos y comprobar si el resultado es correcto. Por otra parte, para desarrollar un programa, una opción es utilizar únicamente el conocimiento informal del programador, comprobando al final, mediante una muestra de datos, si los resultados que se obtienen son correctos y realizando correcciones si es necesario. Siguiendo ese enfoque es difícil asegurar que un programa es realmente correcto. En esta asignatura se presentan métodos matemáticos para verificar la corrección de los programas y para desarrollar programas correctos.

CONTEXTUALIZACIÓN DE LA ASIGNATURA: Esta asignatura se imparte en el segundo cuatrimestre del primer curso. Previamente se han presentado, de manera informal, los fundamentos básicos de la programación imperativa y, por tanto, es el momento apropiado para introducir métodos matemáticos que sirven para diseñar programas correctos y adquirir buenos hábitos de programación. Los conocimientos adquiridos en esta asignatura pueden resultar de gran utilidad en las demás asignaturas que se encargan de profundizar en la programación.

COMPETENCIAS PROPIAS DE LA ASIGNATURA:



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



M02CM08: Capacidad para analizar, diseñar, construir y mantener aplicaciones de forma robusta, segura y eficiente, eligiendo el paradigma y los lenguajes de programación más adecuados.

Tema 1 Introducción: Especificación, corrección y diseño por contrato.

Tema 2 Especificación y documentación formal de programas: Especificación formal pre-post.

Tema 3 Verificación formal de programas: El sistema formal de Hoare.

Tema 4 Derivación formal de programas: Método basado en el sistema formal de Hoare.

Tema 5 Especificación ecuacional (o algebraica) de tipos abstractos de datos.

Tema 6 Transformación formal de programas recursivos: Transformación de recursivo a iterativo.

Durante el desarrollo de las clases se llevarán a cabo, actividades de trabajo en grupo, discusión y

presentación de resultados de ejercicios, con el fin de impulsar la participación directa del alumno en el desarrollo del curso y de

fomentar la motivación del alumnado.

• Sistema de Evaluación Continua
• Sistema de Evaluación Final
• Herramientas y porcentajes de calificación:
  • Prueba escrita a desarrollar (%): 60
  • Realización de prácticas (ejercicios, casos o problemas) (%): 40

EVALUACIÓN CONTINUA:



A lo largo del cuatrimestre se realizarán pruebas (exámenes parciales que constarán de varios ejercicios) para evaluar las distintas competencias trabajadas en cada tema. La superación de un ejercicio supone la liberación de la materia correspondiente. A la hora de contabilizar puntos, solo se tienen en cuenta los ejercicios superados (aquellos en los que se ha alcanzado la mitad de la puntuación correspondiente al ejercicio). La asignatura se aprueba si se alcanzan los 5 puntos. La nota máxima es 10. En concreto, se realizarán cinco exámenes parciales: el examen del Tema 2 valdrá 2 puntos; el examen del Tema 3 valdrá 2 puntos; el examen del Tema 4 valdrá 1,5 puntos; el examen del Tema 5 valdrá 2,5 puntos; finalmente, el examen del Tema 6 valdrá 2 puntos.



En el examen o prueba final (tanto en la convocatoria ordinaria como en la extraordinaria) se evaluarán los temas no liberados y los pendientes de evaluación.



EVALUACIÓN FINAL:

En caso de no elegir la "evaluación continua", al final del cuatrimestre habrá que realizar un examen final que valdrá 10 puntos. Para superarlo bastará con conseguir 5 puntos. También aquí, solo se tendrán en cuenta los ejercicios aprobados (aquellos en los que se ha alcanzado la mitad de la puntuación correspondiente al ejercicio).



NO PRESENTADO:

Se tendrán en cuenta las siguientes normas para decidir cuándo se obtiene "No Presentado": Los alumnos que habiendo optado por la evaluación continua no hayan superado la asignatura mediante las pruebas realizadas durante el cuatrimestre y no se presenten a la prueba o examen final ordinario, tendrán un "No Presentado". Los alumnos que habiendo optado por la evaluación final no se presenten a la prueba o examen final ordinario, tendrán un "No Presentado". En la prueba o examen extraordinario se seguirá el mismo criterio.



CAMBIO EN LA MODALIDAD DE EVALUACIÓN: DE EVALUACIÓN CONTINUA A EVALUACIÓN FINAL:

Los alumnos que hayan optado inicialmente por la "evaluación continua" pueden cambiar a la modalidad de "evaluación final" en cualquier momento previo al examen final (ordinario o extraordinario).



Lo indicado arriba, se ajusta a la "Normativa de Evaluación del Alumnado":

https://www.ehu.eus/es/web/estudiosdegrado-gradukoikasketak/ebaluaziorako-arautegia

Se mantienen los mismos criterios y condiciones indicados para la convocatoria ordinaria.

El material que está a disposición del alumno en la plataforma eGela. Principalmente apuntes y enunciados de los ejercicios de cada tema.

Bibliografía básica

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

Bibliografía de profundización

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.

Revistas

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

Direcciones web

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

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

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