Diseño por Contratos Formal y Verificación

Prerrequisitos: lógica proposicional, funciones, assert.h, TAD y sus invariantes. Este capítulo formaliza los contratos informales del bloque 1.

Objetivo: expresar precondiciones, poscondiciones e invariantes y usarlas para justificar una operación sobre una estructura de datos.

Comprobación de salida: escribí una precondición y una postcondición para una operación de pila y verificá que no se contradigan.

Desarrollo¶

Fundamentos Matemáticos del Diseño por Contratos¶

Para sistemas de software de alta integridad o complejidad (como al implementar las estructuras dinámicas internas de un Tipo de Dato Abstracto), las especificaciones en lenguaje natural o aserciones en tiempo de ejecución resultan insuficientes. Se requiere un marco formal sustentado en la lógica matemática para probar de forma rigurosa la correctitud y coherencia de las rutinas de software.

1. Fundamentos de Lógica de Primer Orden¶

La Lógica de Primer Orden (First-Order Logic, FOL) extiende la lógica proposicional clásica introduciendo cuantificadores sobre elementos individuales del dominio de discurso.

Sintaxis y Alfabeto de la LPO¶

Un lenguaje en Lógica de Primer Orden consta de:

• Variables: Letras que representan elementos genéricos (ej: $x, y, i, j$).

• Conectores lógicos: Negación ($\neg$), conjunción ($\land$), disyunción ($\lor$), implicación ($\rightarrow$), equivalencia ($\leftrightarrow$).

• Cuantificadores: Universal ($\forall$, “para todo”) y Existencial ($\exists$, “existe al menos uno”).

• Constantes y Funciones: Elementos fijos (ej: $0, 1$) o mapeos funcionales (ej: $\text{length}(\text{arr})$).

• Predicados: Relaciones lógicas que evalúan a verdadero o falso (ej: $\text{sorted}(\text{arr})$ o la comparación física de orden $x < y$).

Variables Libres y Ligadas¶

Una ocurrencia de una variable en una fórmula está ligada si se encuentra dentro del alcance directo de un cuantificador ($\forall x$ o $\exists x$). De lo contrario, se considera una variable libre. Una fórmula que carece de variables libres se denomina sentencia.

La operación de sustitución $\phi[t/x]$ representa el reemplazo de todas las ocurrencias libres de la variable $x$ en la fórmula $\phi$ por el término $t$, previniendo la colisión de identificadores.

2. Lógica de Hoare y Cálculo de Precondición Más Débil ($wp$)¶

La Lógica de Hoare provee un sistema axiomático formal para razonar sobre la corrección de algoritmos imperativos mediante el uso de Tripletas de Hoare:

Donde:

• $P$ representa la precondición (aserción sobre el estado antes del programa).

• $S$ representa la secuencia física de instrucciones del programa.

• $Q$ representa la postcondición (aserción que se garantiza verdadera tras la ejecución exitosa de $S$).

Regla de la Asignación¶

La regla de asignación calcula analíticamente la precondición mínima requerida para asegurar una postcondición $Q$ tras asignar una expresión $E$ a la variable $x$:

Precondición Más Débil (Weakest Precondition - $wp$)¶

La precondición más débil $wp(S, Q)$ describe la condición más general (menos restrictiva) sobre el estado inicial del sistema que garantiza que la ejecución de $S$ finalice en un estado que satisfaga la postcondición $Q$.

3. Contratos de Estructuras de Datos e Invariantes de Clase¶

En el diseño de Tipos Datos Abstractos (TADs), un invariante de clase o de estructura es una propiedad lógica fundamental que describe la validez interna de la representación física de los datos. Debe ser verdadera tras la construcción del objeto y preservarse antes y después de cada llamada a métodos o funciones públicas del TAD.

1
2
3
4
5
6
7
8
typedef struct
{
    int *elementos;
    int tope;
    int capacidad;
} pila_t;
// Invariante de estructura Pila:
// elementos != NULL ∧ capacidad > 0 ∧ 0 <= tope <= capacidad

Verificación Práctica: assert.h y la Regla 0x2003h¶

Aunque lenguajes de especificación formal como ACSL son valiosos para verificación estática matemática, en el desarrollo práctico de C (y cumpliendo con las directivas de la cátedra) se utiliza un enfoque pragmático basado en la verificación dinámica con la biblioteca <assert.h> y la documentación estructurada de la Regla 0x2003h: Todas las funciones deben incluir documentación completa y estructurada.

Bajo esta regla, los contratos se establecen de la siguiente manera:

1. Documentación estructurada (@pre y @post): En la cabecera de la función (.h), declarando explícitamente qué asunciones se hacen y qué se garantiza.

2. Verificación dinámica de precondiciones (assert): Al inicio de la implementación de la función (.c), para abortar inmediatamente la ejecución si el cliente viola el contrato en modo desarrollo, evitando que un estado inválido corrompa la memoria.

3. Funciones de validación de invariantes: Implementar una función interna del módulo (ej: bool pila_es_valida(const pila_t *p)) que evalúe y retorne verdadero si todas las invariantes de la estructura de datos se cumplen.

Ejemplo Práctico de Contrato Seguro¶

Archivo de Cabecera (pila.h):

1
2
3
4
5
6
7
8
9
10
11
12
13
typedef struct pila pila_t;
/**
 * Inserta un elemento en el tope de la pila.
 *
 * @param p Puntero a la pila (debe estar inicializada y no estar llena).
 * @param dato Elemento entero a apilar.
 *
 * @pre p != NULL (Regla 0x2003h)
 * @pre p->tope < p->capacidad (La pila no debe estar llena)
 * @post El elemento queda en el tope de la pila y el tamaño se incrementa
 * en 1.
 */
void pila_push(pila_t *p, int dato);

Archivo de Implementación (pila.c):

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
#include "pila.h"
#include <assert.h>
#include <stdbool.h>
#include <stdio.h>
#include <stdlib.h>
struct pila
{
    int *elementos;
    size_t tope;
    size_t capacidad;
};
// Función auxiliar para verificar el invariante del TAD
static bool pila_es_valida(const pila_t *p)
{
    if (p == NULL)
        return false;
    if (p->elementos == NULL)
        return false;
    if (p->capacidad == 0)
        return false;
    if (p->tope > p->capacidad)
        return false;
    return true;
}
void pila_push(pila_t *p, int dato)
{
    // Verificación defensiva y obligatoria de precondiciones en desarrollo
    assert(p != NULL);
    assert(pila_es_valida(p));
    assert(p->tope < p->capacidad);
    // Operación
    p->elementos[p->tope] = dato;
    p->tope++;
    // Verificación de postcondición/invariante
    assert(pila_es_valida(p));
}

El Frame Problem y la directiva assigns¶

El Frame Problem consiste en la dificultad de especificar formalmente qué partes del estado del sistema no cambian durante la ejecución de una función. Sin una solución, las especificaciones deberían listar exhaustivamente cada variable del programa que permanece igual.

En ACSL, esto se resuelve mediante la directiva assigns, la cual especifica con exactitud las únicas variables o posiciones de memoria que la función tiene permitido modificar. El analizador formal asume de manera automática que todo lo que no figure en dicha cláusula permanece inalterado.

Ejercicios de Autoevaluación¶

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
#include <assert.h>
#include <stddef.h>
/**
 * Resetea el valor de la variable apuntada a cero.
 *
 * @param ptr Puntero a la variable entera a resetear.
 *
 * @pre ptr != NULL (Regla 0x2003h)
 * @post El valor apuntado por ptr es igual a 0.
 */
void resetear(int *ptr)
{
    // Verificación dinámica de la precondición
    assert(ptr != NULL);
    *ptr = 0;
    // Verificación de la postcondición
    assert(*ptr == 0);
}

Glosario¶

Síntesis y Resumen¶

En este apunte se han presentado los conceptos fundamentales del tema.

Referencias y Lecturas Complementarias¶

• Meyer, B. Meyer, 1988. Design by Contract. Prentice Hall.

  • El ensayo original que define e introduce la metodología de Diseño por Contrato en la construcción de software robusto.

• Meyer, B. Meyer, 1992. Applying “Design by Contract”. IEEE Computer.

  • Artículo clásico que analiza de forma compacta y pragmática el uso de precondiciones, postcondiciones e invariantes para el control de errores en tiempo de ejecución.

• Meyer, B. Meyer, 1997. Object-Oriented Software Construction (2.ª edición). Prentice Hall.

  • Consultá los capítulos dedicados a la teoría de contratos, herencia y correctitud de algoritmos, que sientan las bases formales del modelado de invariantes de representación.