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