Desarrollo Formal de Software

Comprender los fundamentos de la verificación formal de programas, diferenciándola de las pruebas de software, mediante el estudio de la correctitud parcial y total, los estados de un programa, las aserciones, las precondiciones y postcondiciones, las tripletas de Hoare, la lógica de Hoare y la razón de correctitud, para analizar y justificar formalmente el comportamiento correcto de los programas.

Aplicar técnicas de verificación de programas secuenciales, condicionales y ciclos, mediante el análisis de las instrucciones, las condiciones y los invariantes, para razonar sobre la correctitud del código y la terminación de los programas.

Aplicar técnicas de verificación a programas orientados a objetos, analizando el comportamiento de las clases, los métodos, los objetos y sus interacciones, con el fin de establecer si la implementación cumple las condiciones especificadas y mantiene la correctitud del software.