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