Al finalizar la asignatura el/la estudiante obtendrá los siguientes resultados de aprendizaje:



1. Analizar, diseñar, construir y mantener aplicaciones de forma robusta y segura.

2. Especificar, documentar, validar y verificar programas.

3. Razonar y justificar propiedades relativas a programas.

4. Valorar y comparar especificaciones y documentación de programas desde el punto de vista de la calidad.

5. Conocer la relación entre iteración y recursión la técnica de transformación de programas.

6. Conocer métodos formales de especificación y diseño de programas

Tema 1 Introducción



Tema 2 Especificación de programas

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

Especificación formal pre-post



Tema 3 Verificación de programas

Verificación formal de programas iterativos

Verificación formal de programas recursivos



Tema 4 Tipos Abstractos de Datos



Tema 5 Relación entre soluciones recursivas e iterativas

La metodología docente será activa, basada en el seguimiento y evaluación continua. Parte de las sesiones de aula se organizarán según el modelo de seminario y se realizarán discusiones y actividades asociadas a la resolución de casos prácticos.

Durante el desarrollo de la asignatura se utilizarán los métodos del aula invertida, la revisión por pares y las preguntas y test generadas por los estudiantes.

Las actividades en el aula estarán estrechamente unidas a las que se realizarán fuera del horario de clase, tanto trabajando individualmente, como en grupo.

La asignatura tiene dos modos de evaluación: la evaluación final (o de conjunto) y la evaluación continua.



La evaluación continua se oferta a las personas que pueden realizar el seguimiento de la asignatura en el marco establecido de dedicación y asistencia sistemática a las actividades presenciales previstas (clases teóricas y prácticas).



El 90% de la calificación se obtendrá como resultado de tres exámenes, con un peso relativo sobre el total del 27%, 36% y 27%, respectivamente. El 10% restante corresponderá a la realización y entrega, en las sesiones prácticas, de ejercicios o problemas.



Por defecto, el modo de evaluación es la modalidad de evaluación continua. Entre la segunda y tercera prueba escrita correspondientes a la evaluación continua el/la estudiante podrá manifestar explícitamente su deseo de cambiar a evaluación final. Caso de no hacerlo, su inscripción en evaluación continua pasará a ser definitiva.



La calificación en la modalidad de evaluación de conjunto (o basada en el examen final) consiste en la realización de un examen escrito con un peso del 100% o, alternativamente, del 90% de la calificación (las personas que hayan superado la parte práctica en la convocatoria ordinaria podrán optar por mantener su calificación para el 10%).

El que se distribuya al alumnado por medio de la plataforma Moodle de la asignatura.
Notas de clase, material de soporte a la docencia en aula y actividades.

Bibliografía básica

Especificación, Verificación y Derivación Formal de Programas, Pearson (2015),

Alvez J., Arregi X., Gaintzarain J., Lucio P., Maritxalar M.



Algorithms, T.H. Cormen y D. Balkcom, Khan Academy. Accedido Mayo/2023,

https://www.khanacademy.org/computing/computer-science/algorithms



Introduction to Algorithms (cuarta edición) The MIT Press (2022),

Cormen T.H, Leiserson C.E, Rivest R.L. y Stein C.

Bibliografía de profundización

Programazioaren Metodologia, Open Course Ware UPV/EHU (2013),
Alvez J., Arregi X., Lucio P., Maritxalar M.

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

Programación metódica, MacGraw-Hill (1993), Balcázar J.L.
Program Derivation. The Development of Programs from Specifications, Addison-Wesley, (1989), Dromey G.

Revistas

Communications of the ACM:
Retrospective: An Axiomatic Basis For Computer Programming, Octubre 2009
Teach Foundational Language Principles, Mayo 2015
Program Verification: Vision and Reality, Julio 2021