Verificación formal
Last updated
Last updated
Con el fin de dar rigor y formalizar el proceso de verificación, enunciamos a continuación las 6 propiedades que necesitamos demostrar para tener garantía de que un algoritmo es correcto.
La demostración de estas propiedades es, en general, bastante sencilla, y nos asegura la corrección del algoritmo. Obsérvese que todos los símbolos que intervienen en las propiedades anteriores aparecen en el esquema general de las funciones recursivas.
Los puntos 1 y 2 son condiciones que expresan que la función f está bien definida:
La función f ha de estar bien definida dentro del dominio, es decir, la instrucción condicional no aborta en los estados que satisfacen Q.
La función f se invoca siempre en estados que satisfacen su precondición.
Base de la inducción
Paso de la inducción
Los puntos 5 y 6 demuestran que las llamadas que se hacen sobre datos forman una secuencia estrictamente decreciente y finita:
donde 𝑹(𝒔(,) representa la hipótesis de inducción
