A disciplina céntrase no descriptor "verificación formal de programas", isto é, comprobar que un programa satisfai unhas determinadas especificacións (en forma de fórmulas lóxicas) e esté libre de erros, usando a tal fin a proba de teoremas dun xeito similar a como se proba unha propiedade matemática. A asignatura contempla tamén a derivación de programas a partir da súa especificación formal: noutras verbas, as fórmulas convírtense na guía para obter o programa final que as satisfai.
(*)A Guía docente é o documento onde se visualiza a proposta académica
da UDC. Este documento é público e non se pode modificar, salvo casos excepcionais baixo a revisión do
órgano competente dacordo coa normativa vixente que establece o proceso de elaboración de guías
Asignaturas
