| Competencias do título |
| Código | Competencias da titulación |
| A4 | Interpretar as especificacións funcionais encamiñadas ao desenvolvemento das aplicacións informáticas. |
| A7 | Realizar probas que verifiquen a validez funcional, a integridade dos datos e o rendemento das aplicacións informáticas. |
| B2 | Resolver problemas de forma efectiva. |
| B3 | Aplicar un pensamento crítico, lóxico e creativo. |
| B4 | Aprendizaxe autónoma. |
| B5 | Traballar de forma colaborativa. |
| B12 | Capacidade para a análise e a síntese. |
| Resultados de aprendizaxe | |||
| Competencias de materia (Resultados de aprendizaxe) | Competencias da titulación | ||
| - Aprender a usar os métodos formáis e o razoamento lóxico para a verificación e o deseño de programas. | A4 A7 |
B2 B3 B12 |
|
| - Acostumarse a especificar formalmente os requisitos dun programa, escribindo en fórmulas a súa precondición e postcondición. | A4 |
B3 B12 |
|
| - Adquirir soltura coa construcción de probas formáis tanto en lóxica proposicional como en lóxica de predicados e uso de cuantificadores. | A7 |
B2 |
|
| - Aprender a deseñar programas correctos a partir da súa especificación formal e a proba de corrección da mesma. | A4 A7 |
B2 B4 B5 |
|
| Contidos |
| Temas | Subtemas |
| Introducción |
Un pouco de historia Algúns exemplos |
| Lóxica | Cálculo proposiconal Cálculo de predicados |
| Notación para arrays | Notación Abreviaturas Arrays multidimensionais |
| Guarded Command Language | Sintaxis Semántica operacional Algunhas definicións: determinismo, equivalencia Funcións e procedementos |
| Verificación Formal de Programas | Corrección parcial vs total Semántica axiomática de GCL Proba de corrección de sentencias condicionais Proba de corrección de bucles: invariante e función cota |
| Derivación de Programas | Estratexias para a construcción de condicionais Estratexias para a construir un bucle a partir da invariante e a cota |
| Detección de invariantes | Estratexias para o deseño de invariantes |
| Deseño de Funcións Cota | Estratexia para o deseño de funcións cota Detección de orde lexicográfica na evolución das variables |
| Procedementos, Funcións e Recursividade | Proba de corrección con paso de parámetros Tipos de Recursividade Proba de corrección para chamadas a funcións recursivas |
| Planificación | |||
| Metodoloxías / probas | Horas presenciais | Horas non presenciais / traballo autónomo | Horas totais |
| Prácticas de laboratorio | 20 | 40 | 60 |
| Proba obxectiva | 0 | 30 | 30 |
| Sesión maxistral | 45 | 0 | 45 |
| Traballos tutelados | 0 | 10 | 10 |
| Atención personalizada | 5 | 0 | 5 |
| *Os datos que aparecen na táboa de planificación son de carácter orientativo, considerando a heteroxeneidade do alumnado | |||
| Metodoloxías |
| Metodoloxías | Descrición |
| Prácticas de laboratorio | Elaboración por parte de grupos (máximo dúas persoas) dunha práctica de programación e especificación formal. O profesor presenta inicialmente a linguaxe a utilizar e o enunciado da práctica. Posteriormente os alumnos traballan no laboratorio e requiren a axuda do profesor para solventar as dificultades que encontran ou resolver as dudas sobre a resolución do exercicio. A práctica é obligatoria e computa un 10% do resultado final da avaliación. |
| Proba obxectiva | Trátase dun exame escrito no que se avalían as capacidades do alumno e os coÑecementos adquiridos ao largo do curso. O exame consta de distintos exercicios: unha proba de resposta múltiple, e varios exercicios de desenrolo. Un destes exercicios valórase nun 10% da calificación final e pode ser sustituído por un traballo tutelado optativo. |
| Sesión maxistral | Inclúe as seguintes actividades. (1) Exposición en clase do temario por parte do profesor. (2) Resolución de exercicios en pizarra por parte do profesor e dos alumnos de xeito voluntario. (3) Resolución de dudas en grupo. |
| Traballos tutelados | Son traballos de resolución de exercicios similares aos da pizarra e aos da proba obxectiva, pero dun volume maior. Se realizan por grupos (máximo de dúas persoas) e son optativos. Conlevan o uso de horas de tutorías (atención persoalizada) para supervisar a evolución dos alumnos. Computan na avaliación final cun máximo dun 10%, xa que permiten reemplazar a un dos exercicios da proba obxectiva con esa mesma calificación. |
| Atención personalizada |
|
|
| Avaliación | ||
| Metodoloxías | Descrición | Cualificación |
| Prácticas de laboratorio | Son obrigatorias e computan un máximo de un punto sobre os 10 totais. | 10 |
| Proba obxectiva | É obrigatoria, e computa un máximo de 9 puntos sobre os 10 totais. Para aprobala, é imprescindible obter un mínimo de 4'5 puntos. NOTA: Un dos exercicios da proba valorado nun máximo de un punto, pode ser reemplazado por un traballo tutelado. | 80 |
| Traballos tutelados | Son voluntarios e optativos, poden realizarse en grupos de ata dúas persoas e computan un máximo de 1 punto sobre os 10 totais. Ese punto reemplaza a un dos exercicios da proba obxectiva, coa mesma puntuación. | 10 |
| Observacións avaliación | ||
| Fontes de información |
| Bibliografía básica |
R. Peña Marí (). Diseño de programas. Formalismo y abstracción. Addison-Wesley
J. L. Balcázar (). Programación Metódica. McGraw-Hill
David Gries (). The Science of Programming. Springer-Verlag |
|
|
|
| Bibliografía complementaria |
D. Arnow, G. Weiss (). Introducción a la programación con Java. Addison-Wesley
P. Naughton (). Manual de Java. McGraw-Hill |
|
|
| Recomendacións | |
| Materias que se recomenda ter cursado previamente |
| Materias que se recomenda cursar simultaneamente |
| Materias que continúan o temario |
| Observacións | |