Computaci¿in memoria Aut¿as y traductores finitos. Lenguajes y expresiones regulares. Aplicaciones: an¿sis l¿co

Memoria con restricciones Aut¿as con pila. Gram¿cas y lenguajes incontextuales. Aut¿as lineales acotados. Aplicaciones: an¿sis sint¿ico.

El modelo general de computador y sus limitaciones M¿inas de Turing. Universalidad computacional y Tesis de Church-Turing. Incomputabilidad. Introducci¿ la complejidad computacional. Aplicaciones: criptograf¿de clave p¿blica.

Alternativas al modelo de computaci¿odelos de m¿ina y paradigmas de programaci¿Circuitos y m¿inas reales. Programas imperativos, funcionales y l¿os. Aplicaciones: razonamiento autom¿co

Alternativas al modelo de problema Especificaciones no funcionales. ¿rboles de decisi¿Clasificadores. Programaci¿robabil¿ica. Aplicaciones: sistemas que aprenden.

En las clases magistrales (M) se describen los diferentes fundamentos te¿os de la asignatura, introduci¿ose algoritmos a modo de ejercicios resueltos en clase. Se proponen nuevos ejercicios a ser resueltos en grupos de dos en los laboratorios (PL), cuya comprobaci¿e realizar¿ediante simuladores de aut¿as (JFLAP).

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

Para aprobar la asignatura es necesario obtener al menos cinco puntos sobre 10.



* Pruebas escritas - Evaluaci¿ontinua

Dentro de la evaluaci¿ontinua se realizar¿tres ex¿nes parciales del 75% de la nota de la asignatura. Para la convocatoria ordinaria se permitir¿resentarse a una repesca opcional de los dos primeros bloques para mejorar la nota. Para poder aprobar la convocatoria ordinaria habr¿ue obtener al menos un 25% de la nota en cada uno de los dos primeros parciales y un 15% en el tercero.



* Evaluaci¿e los laboratorios - Evaluaci¿ontinua

Dentro de la evaluaci¿ontinua se valorar¿on un 25% de la nota los laboratorios, realiz¿ose pruebas individualizadas tras su finalizaci¿No habr¿ota m¿ma ni ser¿bligatorio presentarse. A modo de ejemplo, quien no se presente a ninguna evaluaci¿e laboratorios solo podr¿ptar a una nota m¿ma de 7,5.



* Evaluaci¿inal (100%)

Si se renuncia a la evaluaci¿ontinua se realizar¿n examen final del 100% de la nota. Esta renuncia deber¿er notificada al profesor antes de la 9¿ semana de acuerdo con la normativa existente. No se guarda ninguna nota. Ser¿ecesario obtener al menos un 15% de la nota en cada uno de los tres bloques correspondientes a los parciales de la evaluaci¿ontinua.



* No presentado

Si no se asiste a la evaluaci¿inal (100% o tercer parcial con repescas) se considerar¿o Presentado.



* Evaluaci¿o presencial

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

Para la convocatoria extraordinaria se realizar¿n examen final del 100% de la nota.



No se guarda ninguna nota de evaluaciones anteriores.



Ser¿ecesario obtener al menos un 15% de la nota en cada uno de los tres bloques correspondientes a los parciales de la evaluaci¿ontinua.



* Evaluaci¿o presencial

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

Se proporcionar¿n eGela el siguiente material de uso obligatorio: Presentaciones de la asignatura Ejemplos resueltos de la asignatura Ejercicios de la asignatura Simulador JFLAP proporcionado

Bibliografía básica

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

Bibliografía de profundización

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

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