Please enable JavaScript.
Coggle requires JavaScript to display documents.
Verificación Formal de Programas - Coggle Diagram
Verificación Formal de Programas
Fundamentos de la Verificación Formal
Objetivo: Demostrar matemáticmente que un programa cumple su especificación.
Especificación: Dada mediante precondición (Q) y postcondición (R).
Herramienta principal: Lógica de Hoare
Triplas de Hoare {Q} P {R}.
Si Q es verdadera antes de ejecutar P, y P termina, entonces R será verdadera al final.
Componentes: Q: Precondición (estado inicial válido). P: Programa o fragmento de código. R: Postcondición (estado final deseado)
Tipos de corrección: Corrección parcial: Si el programa termina, entonces R se cumple. --> No garantiza terminación. Corrección total: El programa termina y R se cumple. --> Requiere función cota (para ciclos)
Reglas de Inferencia para Construir Triplas
Instrucción vacía (skip). Semántica: No hace nada. Regla: :checkered_flag: {R} skip {R} --> La precondición y las postcondición son iguales.
Asignación (X:=E). Regla :checkered_flag: de asignación: {R[E/x]} x:= E{R} --> Reemplazar todas las ocurrencias de x por E en R. Ejemplo: {x+1=5} x:= x+1 {x=5}
Precondición más débil (WP). Definición: La condición inicial memos restrictiva que garantiza R tras ejecutar P. Notación: wp(P, R). Ejemplos: wp(x:=E, R) = R[E/x]. wp(skip, R) -->R
Composición secuencial (P1; P2). Regla: :checkered_flag: Si {Q} P1 {M} y {M} P2 {R}, entonces {Q} P1; P2 {R}. WP: wp(P1; P2, R) = wp(P1, wp(P2, R))
Instrucción condicional (If B then P1 else P2). Regla: :checkered_flag: Si {Q ∧ B} P1 {R} y {Q ∧ ¬B} P2 {R}, entonces {Q} if B then P1 else P2 {R}. WP:
Verificación de Programas Iterativos (while) {Q} while B do P {R}
Invariante de Ciclo (P_inv). Definición: Predicado que: :check: es verdadero antes del ciclo. :check: Se mantiene verdadero tras cada iteración. :check: Al salir del ciclo ¬B , junto con P_Inv, implica la postcondición. Regla: :checkered_flag: Si {P_inv ∧ B} P {P_inv}, entonces {P_inv} while B do P {P_inv ∧ ¬B}
Precondición --> Invariante. Debe probarse: Q ⇒ P_inv
Invariante + ¬B ⇒ Postcondición. Debe probarse P_inv ∧ ¬B ⇒ R
Teorema de Invarianza. Si un predicado es verdadero antes de un ciclo y se mantiene tras cada iteración, entonces es verdadero al salir del ciclo.
Corrección Total: Función Cota (Terminación).
Función Cota (t). Requisitos: :fire: t es una expesión entera. :fire: t ≥ 0 en cada iteración. :fire: t disminuye estrictamente en cada iteración. :fire: Existe un mínimo conocido (T_min, ej: 0). Conclusión: el ciclo termina.
Corrección total = Corrección parcial + Terminación.
Estrategia General para Verificar un Programa.
Especificar: Definir Q y R.
Descomponer: Analizar estructura (secuencial, condicional, iterativa).
Para ciclos: :check: Proponer invariante y cota. :check: Validar las tres propiedades del invariante. :check: Verificar que la cota cumple sus condiciones.
Aplicar reglas recursivamente (de abajo hacia arriba o con wp).