Semántica y Verificación
GRUPO 7014
2023-1
Prof. Lourdes del Carmen González Huesca ma ju 13 a 14:30 P118
Ayud. Braulio Aaron Santiago Carrillo lu mi 12 a 13 P118
Conocimientos deseables:
Lenguajes de Programación, Lógica computacional.
Temario:
Introducción: importancia de la semántica en lenguajes de programación; visión general de los métodos semánticos.
Propiedades de las descripciones semánticas; composicionalidad e inducción.
Un lenguaje imperativo-funcional.
Semántica operacional: semántica de paso pequeño y de paso grande; sistemas de tipos.
Semántica axiomática: análisis de invariantes, Lógica de Hoare.
Semántica denotacional: interpretación denotacional; introducción a la teoría de puntos fijos.
Evaluación:
70% Tareas teórico-prácticas (6) usando el asistente de pruebas Coq
fechas tentativas de entregas (jueves) : 1sept -- 22 sept -- 6oct -- 27oct -- 17 nov -- 8 dic
30% Actividades complementarias (lecturas o cuestionarios)
No hay reposición de ninguno de los anteriores, ni hay examen final.
No se elimina la calificación más baja de ninguno aunque puede hacerse una excepción al final.
Para tener derecho a calificación final aprobatoria es necesario tener un promedio aprobatorio de tareas.
Para obtener un NP es necesario que no se tengan más de dos calificaciones de cualquier tipo.