Diseño por Contratos Formal y Verificación

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

Introducción¶

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

ACSL (ANSI/ISO C Specification Language)¶

ACSL permite escribir anotaciones formales directamente en los comentarios del código de C para su verificación estática mediante analizadores como Frama-C:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
/*@ predicate pila_valida(pila_t *p) =
        \valid(p) &&
        p->elementos != NULL &&
        p->capacidad > 0 &&
        0 <= p->tope <= p->capacidad &&
        \valid(p->elementos + (0..p->capacidad-1));
  */

/*@ requires pila_valida(p);
    requires p->tope < p->capacidad;
    assigns p->tope, p->elementos[p->tope];
    ensures pila_valida(p);
    ensures p->tope == \old(p->tope) + 1;
    ensures p->elementos[p->tope - 1] == dato;
  */
void push(pila_t *p, int dato);

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¶

/*@ requires \valid(ptr);
    assigns *ptr;
    ensures *ptr == 0;
 */
void resetear(int *ptr);

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.