- Capacidad para analizar, dise¿ 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¿e programas desde el punto de vista de la calidad

- Conocimiento de m¿dos formales de especificaci¿ dise¿e programas

- Conocimiento de las nociones b¿cas en sem¿ica axiom¿ca de lenguajes de programaci¿- Conocimiento y aplicaci¿e los procedimientos algor¿icos b¿cos de las tecnolog¿ inform¿cas para dise¿soluciones a problemas, analizando la idoneidad y complejidad de los algoritmos propuestos



Objetivos espec¿cos:

- Especificaci¿correcci¿ dise¿or contrato

- Especificaci¿ormal pre-post

- El sistema formal de Hoare

- La t¿ica de especificaci¿cuacional

- El m¿do de derivaci¿ormal

Tema 0: Introducci¿Tema 1: Aserciones L¿as

Tema 2: Especificaci¿Tema 3: Verificaci¿Tema 4: Derivaci¿

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



En las clases de ejercicios se desarrollar¿un conjunto de ejercicios. Los ejercicios a realizar plantean problemas inform¿cos que los alumnos deber¿realizar de la forma m¿aut¿a posible.



Durante el desarrollo de las clases se llevar¿a cabo, de forma sistem¿ca, actividades de trabajo en grupo, discusi¿ presentaci¿e resultados de ejercicios, con el fin de impulsar la participaci¿irecta en el desarrollo del curso y de fomentar la motivaci¿el alumnado.

La evaluaci¿e la asignatura en la convocatoria ordinaria se realiza mediante evaluaci¿ontinua o evaluaci¿inal. La opci¿or defecto es la evaluaci¿ontinua salvo que se renuncie a ella.



* Evaluaci¿ediante prueba final:

Se permite renunciar a la evaluaci¿ontinua para realizar la evaluaci¿inal. Esta renuncia se deber¿omunicar al profesorado responsable en los plazos estipulados en el Art¿lo 8 de la normativa sobre la evaluaci¿el alumnado. No se aceptar¿renuncias a la evaluaci¿ontinua posteriores a las fechas habilitadas para ello salvo casos excepcionales.



El examen evaluar¿odo el conjunto de la asignatura. Para aprobar la asignatura, es necesario obtener una calificaci¿¿ma de 5 puntos sobre el total de 10 puntos del examen.



* Evaluaci¿ontinua:

La evaluaci¿or defecto de la asignatura se hace mediante evaluaci¿ontinua, salvo que se haya renunciado expresamente a ella.



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



Pruebas escritas:

1) L¿a 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¿ontinua sin examen final

- Realizar todas las pruebas escritas

- Nota m¿ma de 5 en la suma de todas las pruebas

- Nota m¿ma de 25% en cada una de las pruebas



* Examen final ordinario de la convocatoria ordinaria:



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



El examen se dividir¿n cuatro partes correspondientes a cada prueba:

- Se podr¿realizar las partes que se deseen

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

- Se perder¿a nota de las pruebas anteriormente realizadas, correspondientes a las partes que se realicen en este examen, a efectos del c¿ulo 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¿ma de 5 en la suma de todas las pruebas escritas

- Nota m¿ma de 25% en cada prueba escrita



* Renuncia al derecho al examen:

El alumnado que sigue la evaluaci¿ontinua podr¿ealizar la renuncia a la convocatoria de acuerdo con lo estipulado en el Art¿lo 12 de la normativa sobre la evaluaci¿el alumnado.



El alumno que no se presente a dos o m¿pruebas escritas en la convocatoria ordinaria, obtendr¿omo calificaci¿inal "No Presentado", independientemente de que haya realizado, o no, el resto de pruebas escritas y/o actividades del curso.



* Casos de copia:

Se aplicar¿l Art¿lo 11 de la normativa vigente referente a la evaluaci¿el alumnado.



Si no se puede realizar una evaluaci¿resencial de la asignatura, se realizar¿los cambios pertinentes para hacerlo online mediante la utilizaci¿e las herramientas inform¿cas existentes en la UPV/EHU. Las caracter¿icas de esta evaluaci¿nline ser¿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¿Verificaci¿ Derivaci¿ormal de Programas. J. ¿lvez, X. Arregi, J. Gaintzarain, P. Lucio y M. Marichalar, Pearson, 2016.

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

- Metodolog¿y Tecnolog¿de la Programaci¿I. M. D¿ Roca, J. C. Rodr¿ez del Pino. Univ. Palmas Gran Canaria, 2004.

- Verificaci¿e Programas y Metodolog¿de la Programaci¿A. D¿ de Ilarraza, P. Lucio. Servicio Editorial Universidad del Pa¿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¿et¿a. J.L. Balc¿r. MacGraw-Hill, 1993. - Dise¿e Programas.- Formalismo y Abstracci¿Ricardo Pe¿Prentice Hall, 1998.

Aldizkariak

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