Introducción al Diseño por Contrato

Prerrequisitos: funciones, assert, condicionales y lectura de firmas en C.

Objetivos: 1. Diferenciar precondición, postcondición e invariante. 2. Documentar el contrato de una función pequeña.

Comprobación de salida: señalá qué obligación corresponde al llamador y cuál a la función en un contrato propuesto.

Introducción al Diseño por Contrato¶

Introducción¶

El Diseño por Contrato (Design by Contract, DbC) es una metodología de desarrollo de software formalizada por Bertrand Meyer. Propone que la interacción entre diferentes partes de un sistema (por ejemplo, el código que llama a una función y la función misma) se debe modelar como un contrato formal entre clientes y proveedores.

Un contrato establece derechos y obligaciones mutuas. En el contexto de las funciones, los componentes clave de este acuerdo son las precondiciones, postcondiciones e invariantes.

Precondiciones y Postcondiciones Informales¶

Precondiciones y postcondiciones son las dos caras de una misma obligación: qué debe garantizar quien llama a una función antes de invocarla, y qué debe garantizar la función a cambio, si esa condición de entrada se cumplió.

Precondiciones (El Derecho del Proveedor, Obligación del Cliente)¶

Una precondición especifica las condiciones que deben ser obligatoriamente verdaderas antes de que una función comience su ejecución.

• Obligación del Cliente: El código que llama a la función es responsable de garantizar que los argumentos y el estado del sistema cumplan la precondición.

• Derecho del Proveedor: El programador que implementa la función puede asumir libremente que la precondición se cumple. No tiene la obligación de verificarla ni de manejar situaciones donde no sea verdadera.

• Consecuencia de Violación: Si la precondición se viola, el comportamiento del programa es indefinido (undefined behavior). El programa puede fallar catastróficamente, corromper memoria o retornar resultados absurdos.

1
2
3
4
5
6
7
// Precondición: 'b' no debe ser cero.
int dividir(int a, int b)
{
    // Si b es cero, la división por cero provocará un fallo físico en el
    // hardware.
    return a / b;
}

Postcondiciones (El Derecho del Cliente, Obligación del Proveedor)¶

Una postcondición describe las garantías lógicas que la función promete cumplir después de terminar su ejecución, siempre y cuando la precondición haya sido satisfecha al inicio.

• Obligación del Proveedor: La función debe garantizar que el valor devuelto y las modificaciones de estado cumplan la postcondición.

• Derecho del Cliente: El código llamador puede asumir con total certeza que el resultado es válido y proceder en consecuencia.

1
2
3
4
5
6
7
// Precondición: 'radicando' >= 0
// Postcondición: El valor retornado es 'r' tal que r * r <= radicando y
// (r+1)*(r+1) > radicando
int raiz_entera(int radicando)
{
    // Implementación del algoritmo
}

Verificación Dinámica de Contratos en C¶

En el lenguaje C, el contrato se documenta formalmente en la cabecera de la función de acuerdo con la regla 0x2003h: Todas las funciones deben incluir documentación completa y estructurada (que exige documentar precondiciones y postcondiciones de manera estructurada). Sin embargo, además de documentarse de forma textual, es una excelente práctica de diseño defensivo verificar dinámicamente las precondiciones usando la macro assert() de <assert.h>.

Por ejemplo, la función raiz_entera puede implementarse validando su precondición:

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
#include <assert.h>
/**
 * @brief Calcula la raíz cuadrada entera de un número.
 * @pre radicando >= 0 (Regla 0x2003h)
 * @post retorna 'r' tal que r * r <= radicando y (r+1)*(r+1) > radicando
 */
int raiz_entera(int radicando)
{
    // Verificación dinámica de la precondición
    assert(radicando >= 0);
    int r = 0;
    while ((r + 1) * (r + 1) <= radicando)
    {
        r++;
    }
    return r;
}

Invariantes Elementales e Invariantes de Lazo¶

Invariantes de Lazo (Loop Invariants)¶

Un invariante de lazo es una condición lógica (una afirmación sobre las variables del programa) que es verdadera:

1. Antes de ingresar al lazo de control.

2. Antes y después de cada iteración individual del lazo.

3. Inmediatamente después de salir del lazo de control.

Los invariantes de lazo son la herramienta didáctica fundamental para razonar lógicamente sobre la correctitud de los algoritmos iterativos. Nos permiten verificar de forma inductiva que un lazo de control realmente cumple su objetivo paso a paso.

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
// Precondición: arr != NULL y n >= 0
// Postcondición: retorna la suma de todos los elementos de arr[0] a arr[n-1]
int sumar_arreglo(const int arr[], int n)
{
    int suma = 0;
    int i = 0;
    // Invariante: suma es la suma acumulada de arr[0] a arr[i-1] AND 0 <= i <=
    // n
    while (i < n)
    {
        suma += arr[i];
        i++;
    }
    return suma;
}

• Inicialización (Paso Base): Antes de la primera iteración, $i = 0$, por lo que la suma acumulada de $arr[0]$ a $arr[-1]$ es vacía (valor 0), cumpliéndose el invariante.

• Preservación (Paso Inductivo): Si el invariante se cumple al inicio de la iteración $i$, sumar $arr[i]$ e incrementar $i$ a $i+1$ preserva la relación lógica de acumular la suma hasta la nueva posición del índice.

• Terminación: Al salir del lazo, la condición $i < n$ es falsa. Como el invariante asegura que $i \leq n$, deducimos que $i = n$. Sustituyendo esto en el invariante, concluimos que suma almacena la suma de $arr[0]$ a $arr[n-1]$, lo cual satisface la postcondición de la función.

Ejercicios de Autoevaluación¶

Precondiciones y Postcondiciones¶

Invariantes de Lazo¶

Glosario¶

Síntesis y Resumen¶

En esta unidad te introdujiste en el formalismo del Diseño por Contrato y su aplicación en la verificación de algoritmos:

• Relación cliente-proveedor: Documentar precondiciones y poscondiciones divide las responsabilidades del control de errores entre el código llamador (cliente) y la función llamada (proveedor).

• Razonamiento inductivo: El invariante de lazo es la herramienta lógica clave para demostrar de forma rigurosa la correctitud de los algoritmos iterativos. Funciona de manera análoga a la inducción matemática (inicialización, preservación y terminación).

Referencias y Lecturas Complementarias¶

• Meyer, B. (1997). Object-Oriented Software Construction (2nd ed.). Prentice Hall. (Capítulo 11: Design by Contract).

• Meyer, B. (1992). Applying “Design by Contract”. Computer, 25(10), 40-51.

• Gries, D. (1981). The Science of Programming. Springer-Verlag. (Sobre correctitud de programas e invariantes).