VERIFICACIÓN FORMAL DE PROGRAMAS
Proceso de asegurar que un programa cumple con su especificación formal.
Garantizar la corrección del programa antes de su ejecución.^
Del uso de técnicas matemáticas y lógicas.
Ejemplo
Tripla de Hoare
Precondición Más Débil (wp)
Que si la precondición es verdadera antes de la ejecución del programa, entonces la poscondición será verdadera después de la ejecución del programa.
{Precondición} Programa {Poscondición}
El formalismo para la especificación y verificación de programas.
La precondición más débil es la condición más general que garantiza que la poscondición se cumple después de la ejecución del programa.
Determinar la condición inicial mínima necesaria para que el programa sea correcto respecto a su especificación
Se compone de
Instrucciones Básicas
Instrucción Vacía: instrucción que no altera el estado del programa.
Asignación: reemplaza el valor de una variable con el resultado de una expresión.
Instrucción Condicional: permite la ejecución de un conjunto de instrucciones basado en una condición.
Composición Secuencia: ejecución de un conjunto de instrucciones en secuencia.
Proceso de Verificación
Paso 1: identificar la precondición y la poscondición.
Paso 2: derivar la precondición más débil para cada instrucción del programa.
Paso 3: comprobar que la precondición inicial implica la precondición más débil derivada.
Paso 4: validar la tripla {Q}S{R} demostrando que Q ⇒ wp(S, R).
Técnicas de Verificación
Invariantes de Ciclo: propiedades que se mantienen verdaderas en cada iteración de un ciclo.
Verificación Modular: descomponer el programa en módulos y verificar cada uno por separado.
Inducción Matemática: para programas con estructuras repetitivas (ciclos).
Limitaciones y Desafíos
Complejidad: el proceso puede ser complejo y tedioso para programas grandes.
Modelado Correcto: la especificación formal debe ser precisa y completa
Automatización: herramientas de verificación automática pueden ayudar pero no reemplazan el juicio humano.
Herramientas de Verificación
SPARK
Lenguaje y herramienta de verificación para sistemas críticos.
Frama-C
Plataforma para análisis y verificación de código C.
Coq
Asistente de pruebas para el desarrollo de especificaciones formales y pruebas de corrección.
Invariante de Ciclo
Predicado P satisfecho justo antes y después de cada iteración del ciclo.
Proveer información relevante sobre el estado del programa
Cota de Ciclo
Función entera t cuyo valor disminuye con cada iteración del ciclo y está acotada inferiormente
Medir el número de iteraciones restantes del ciclo
Teorema de Invarianza
Regla1: el invariante se cumple antes del inicio del ciclo.
Regla 2: el invariante se cumple justo después de cada iteración del ciclo.
Regla 3: la poscondición se cumple al finalizar la ejecución del ciclo.
Regla 4: la cota del ciclo disminuye con cada iteración.
Regla 5: la cota del ciclo está acotada inferiormente.