Please enable JavaScript.
Coggle requires JavaScript to display documents.
Verificación Formal de Programas : - Coggle Diagram
Verificación Formal de Programas :
(persigue)
Fundamentos y Objetivos
Objetivo: demostrar que el programa cumple su especificación
Tipos de corrección
Corrección parcial (si termina ⇒ Q)
Corrección total (parcial + terminación)
Especificación formal
Precondición (P)
Postcondición (Q)
Estado / efectos / variables modificadas
(se apoya en)
Invariantes de ciclo
Definición: verdad antes/durante/después de cada iteración
Checklist del invariante
Inicialización: P ⇒ I
Conservación: {I ∧ B} S {I}
Utilidad: I ∧ ¬B ⇒ Q
Estrategias para I
Relaciones entre variables
Resumen acumulado (sumas, min/max, prefijos)
Propiedad de segmento (procesado vs por procesar)
Errores comunes
I demasiado débil
Ignorar efectos/variables
No probar conservación
(se ejecuta así)
Metodología paso a paso
Fijar Q
Derivar P mínima
Descomponer por estructuras (seq/if/while)
Proponer y verificar I (ini / conserv / útil)
(Total) Definir V y probar decrecimiento
Componer con reglas de Hoare
Revisar supuestos y casos borde
(se formaliza con)
Lógica de Hoare
Tripla {P} C {Q} (si inicia en P y C termina ⇒ Q)
Reglas de inferencia
Asignación
Secuencia
Condicional (if/else)
While (parcial)
Consequence (fortalecer P / debilitar Q)
Anotación del programa (assert P, I, Q)
(lleva a)
Terminación
Función variante (ranking) a conjunto bien fundado
Obligaciones
I ∧ B ⇒ V > 0
{I ∧ B} S {V' < V}
(recomienda / evitar)
Buenas prácticas y anti-patrones
Aserciones visibles; trazabilidad P/I/Q
Variables lógicas auxiliares
Evitar I tautológico o demasiado específico