Comprender cómo funcionan las construcciones de un lenguaje de programación y ser capaces de describir su comportamiento de forma detallada y precisa.

Aplicar distintas técnicas matemáticas al estudio de los lenguajes de programación y los programas escritos en ellos.
En ocasiones se tratará de teorías y conceptos previamente estudiados y en otras de variantes nuevas, que generarán
una sinergia entre la nueva materia y las otras previamente estudiadas.

- Ser capaces de describir formalmente y analizar el significado de las construcciones básicas de lenguajes de programación
correspondientes a varios paradigmas.
- Ser capaces de distinguir y manejar fluidamente los distintos tipos de inducción que se necesitan para manejar
los distintos tipos de semánticas y relacionarlas entre sí.
- Explicar los conceptos y resultados fundamentales relativos a las semánticas formales de los lenguajes de programación.
- Comparar diferentes descripciones semánticas de un mismo lenguaje de programación, entendiendo el sentido en que
son equivalentes y la forma en que se complementan.
- Derivar distintas consecuencias que se siguen de las descripciones semánticas.
- Aplicar lo aprendido para elaborar la definición de otros lenguajes de programación o construcciones adicionales de los mismos.
- Aplicar lo aprendido para precisar el significado de programas concretos y en base a ello probar la corrección de los mismos..

Exposición por parte del profesor de los conceptos y resultados más importantes de cada tema. Estas exposiciones serán ilustradas con
ejemplos y ampliadas a partir de las observaciones y preguntas de los alumnos. Estudio por parte de los alumnos del resto de la materia,. trasladando en su caso sus dudas o comentarios en las clases siguientes o asistiendo a las tutorías para que el profesor la clarifique cuando resulte necesario.
El estudio personal incluirá la resolución inmediata de aquellos ejercicios introducidos por los autores del texto que seguiremos a lo largo de cada tema, para que sirvan de "autoevaluación" dejando de manifiesto que se va entendiendo y aprendido la materia.

De disponer de tiempo para ello, a lo largo del curso el profesor expondrá las ideas fundamentales de diversos temas complementarios que se proponen como trabajos "voluntarios" a fin de aumentar aún más la nota
de evaluación continua conseguida según los cauces obligatorios que se detallan abajo.

La mayor parte de ellas, sin previo aviso, comenzarán con la propuesta de algún ejercicio sencillo que deberá ser resuelto y entregado en un breve periodo de tiempo. Los ejercicios buscarán poner de manifiesto simplemente que la asignatura se va llevando al día, lo que se considera necesario y suficiente para poder sacar partido a las clases siguientes. Los ejercicios se calificarán devolviéndose posteriormente a los alumnos para que sean conocedores del grado de asimilación de la materia y la consiguiente materialización del mismo en la parte correspondiente de su evaluación continua.

A continuación se comentarán las soluciones aportadas por los alumnos a esos ejercicios sencillos en el texto, y por último cuando aparezcan ya problemas de una cierta entidad se darán en clase las ideas fundamentales para resolverlos, urgiendo a los alumnos a completar sus soluciones, para más tarde compararlas con las que el profesor aportará en el Campus con todo detalle, para que los alumnos capten la total importancia que el rigor tiene en materias como la presente, y vaya adquiriendo la habilidad de incorporarlo en sus propias soluciones.

2

4

8

Estudio de las semánticas formales para los lenguajes de programación.
Conceptos fundamentales que soportan las distintas semánticas y las
relaciones entre las mismas.
Utilización de los formalismos para describir la semántica de construcciones
de los lenguajes, calcular la semántica de programas y analizar las propiedades
de los mismos. probando en particular su corrección.
Aplicaciones.

Es altamente recomendable haber cursado Lógica Matemática. También son útiles algunos de los conceptos estudiados en Programación declarativa, Estructuras de datos y Diseño de algoritmos.

Mostrar al alumno la necesidad de contar con definiciones formales del significado de los lenguajes de programación,
que permitan precisar lo que calcularán, y cómo, los programas escritos usando los mismos. A partir de ellas se podrá razonar
sobre su corrección con respecto a una especificación dada.
Ofrecer al alumno un campo interesante para aplicar distintas técnicas y conceptos matemáticos aprendidos
durante la carrera, viendo como utilizarlas para definir la semántica de los lenguajes de programación

- Inducción en sus distintas variantes.

- Semántica operacional, denotacional y axiomática para un lenguaje imperativo sencillo.

- Aplicaciones.

- Elementos que permiten definir el significado de construcciones más complejas.

La metodología que se aplicará exigirá la participación activa del alumno en el "día a día", buscándose
un aprendizaje "continuo" que se pondrá de manifiesto a través de dicha participación.
Un 40% de la nota se conseguirá en base a dicha participación activa a distintos niveles:

Ejercicios entregados EN las clases prácticas (la mitad de ese 40%): sin previo aviso, la mayor parte de esas clases comenzarán con la propuesta de algún ejercicio sencillo, que deberá ser resuelto y entregado en un breve periodo de tiempo. Los ejercicios buscarán poner de manifiesto simplemente que la asignatura se va llevando al día, y se devolverán corregidos en un breve periodo de tiempo.

Participación en las clases teóricas (planteando preguntas, comentarios, etc.)
Ejercicios, tanto sencillos como más complicados, que podrán ser incorporados a un Cuaderno de Ejercicios personal en el CVirtual, aparte de ser discutidos en las clases prácticas. Estas aportaciones NO se evaluarán, pero se tendrá en cuenta su realización, mejor a su debido tiempo. Sin embargo los alumnos podrán utilizar las tutorías para discutir con el profesor sus soluciones, en especial cuando les queden dudas sobre su corrección técnica.

La realización de los trabajos voluntarios podrá incrementar la nota de este segundo 20% de la nota final.

El examen final, donde se espera que el alumno ratifique la adquisición de las competencias descritas anteriormente, generará un 60% de la nota. Salvo posibles excepciones muy justificadas a ser evaluadas por el profesor, el baremo se mantendrá en la convocatoria extraordinaria, siendo posible presentar ejercicios y trabajos para la misma de manera análoga a como para la ordinaria. Sin embargo, la parte de la nota correspondiente a la participación en las clases, al corresponder con lo realizado durante el curso, no será modificable.

No se exigirá ninguna nota mínima en ninguna de las partes: tan sólo conseguir el 5 entre los tres apartados

- Hanne Riis Nielson y Flemming Nielson, Semantics with Applications. An Appetizer, Springer, 2007.
- Glynn Winskel, The Formal Semantics of Programming Languages, The MIT Press, 1993.

La asignatura dispondrá de un espacio en el Campus virtual que albergará la documentación que se considere oportuna.
Se facilitarán "transparencias" como guión para facilitar el estudio de la asignatura fuera de las clases, pero en modo alguno se podrá considerar que por medio de las mismas "se cubre" la materia del curso y por tanto se puede suplir la asistencia a clase, que como queda dicho se considera absolutamente fundamental para superar la asignatura.