Introducción a la verificación formal con SPARK ── De los contratos de Ada a la demostración matemática

1. Introducción ── Más allá de «ejecutar y comprobar»

La forma más habitual de garantizar la calidad del software son las pruebas.

Prueba: verifica que el programa se comporte correctamente para las entradas seleccionadas

Pero las pruebas tienen límites. El número de combinaciones de entradas es infinito, y las pruebas por sí solas no pueden demostrar que el programa es correcto para todas ellas.

Aquí es donde entra en juego la verificación formal (Formal Verification).

Verificación formal: demuestra matemáticamente que una propiedad se cumple para todas las entradas posibles

El artículo anterior, «El atractivo del lenguaje Ada», presentó una visión general de Ada y mencionó SPARK brevemente.

En este artículo nos centramos en la práctica de la verificación formal con SPARK y organizamos los siguientes puntos:

Qué es SPARK y cuál es su relación con Ada
Cómo escribir contratos (Pre/Post)
Cómo demostrar con GNATprove
Cómo diseñar invariantes de bucle
Cómo gestionar los efectos secundarios con contratos de flujo de datos (Global/Depends)
La estrategia de aplicación progresiva de los niveles de demostración (Stone a Platinum)
Cómo incorporarlo en un proyecto real

El objetivo es que pueda experimentar, con ejemplos de código reales, el paso de las pruebas a la demostración.

El público y los conocimientos previos para este artículo

Los lectores previstos son personas como las siguientes:

• Quienes ya han visto alguna vez la sintaxis básica de Ada (paquetes, los modos de parámetro in / out / in out, los tipos y subtipos)
• Quienes se interesan por la programación por contrato y el análisis estático, y buscan «el siguiente paso después de las pruebas»
• Quienes evalúan mecanismos de garantía de calidad para software de alta fiabilidad, empotrado o de control

Se puede leer sin experiencia previa en Ada, pero conviene aclarar dos requisitos. Los ejemplos de código de este artículo recurren repetidamente a la separación entre la especificación y el cuerpo de un paquete mediante package ... is y package body ... is, y a modos de parámetro como procedure P (X : in out Integer). Si estas dos cosas no le resultan familiares, conviene repasar antes los fundamentos de Ada en «El atractivo del lenguaje Ada» y volver después, para poder concentrarse en los contratos.

Dicho de otro modo, con entender solo estas dos cosas se puede seguir el artículo. La notación propia de SPARK (SPARK_Mode, Pre, Post, Loop_Invariant, Global, Depends) se explica por completo dentro de este artículo. Tampoco hace falta conocer la teoría de los demostradores ni la lógica formal: lo único necesario en la práctica es leer los mensajes que da GNATprove y corregir el código o el contrato.

Los fragmentos de código que aparecen en este artículo están además publicados en GitHub como una colección de referencia organizada por capítulos.

ada-spark-formal-verification - komurasoft-blog-samples (GitHub)

2. Qué es SPARK ── el subconjunto de Ada que abre la puerta a la demostración

SPARK es un subconjunto (lenguaje parcial) de Ada.

Ser un subconjunto responde a una intención clara.

Todas las funciones de Ada → gran expresividad, pero verificarlo todo formalmente no es realista
SPARK                       → se limita a las funciones verificables, para que la demostración sea realista

Las principales restricciones que impone SPARK son las siguientes.

Gestión dinámica de memoria mediante punteros (tipos de acceso) → controlada mediante un modelo de propiedad
Uso libre de manejadores de excepción                            → permitido con restricciones
Estructuras de datos recursivas                                  → restringidas porque dificultan la demostración
Uso libre de tareas                                               → restringido mediante el perfil Ravenscar

Oír la palabra «restricción» puede sonar limitante. Pero estas restricciones se obtienen a cambio de la demostrabilidad.

El conjunto de herramientas de SPARK gira en torno a GNATprove, proporcionado por AdaCore.

Funcionamiento de GNATprove:
1. Analiza el código Ada escrito en SPARK
2. Convierte los contratos (Pre/Post) y las aserciones al lenguaje intermedio Why3
3. Intenta demostrarlos con probadores automáticos como Z3, cvc5 y Alt-Ergo
4. Informa del resultado como mensajes ubicados en el código fuente

Como diagrama, el flujo es el siguiente.

flowchart LR
    Src["Código Ada escrito en SPARK<br/>Pre / Post / Assert"] --> GP[GNATprove]
    GP --> VC[Generación de condiciones de verificación]
    VC --> Why3["Why3<br/>lenguaje intermedio y plataforma de demostración"]
    Why3 --> P1[cvc5]
    Why3 --> P2[Z3]
    Why3 --> P3[Alt-Ergo]
    P1 --> Res[Agregación de resultados]
    P2 --> Res
    P3 --> Res
    Res --> Msg["Mensajes ubicados en el código fuente<br/>info / medium / high"]

El desarrollador solo toca directamente los dos extremos: el código de la izquierda y los mensajes de la derecha. Why3 y los demostradores del centro funcionan de forma automática, así que normalmente no hace falta prestarles atención — solo cuando la demostración no pasa y hay que cambiar de demostrador o darle más tiempo.

Nombres que han aparecido en este capítulo

Aquí fijamos los términos que aparecen por primera vez. A partir de ahora se usan sin explicación adicional.

Lo importante es que SPARK está construido sobre Ada.

Código SPARK = código Ada + anotaciones de contrato

Es decir, SPARK se sitúa en la prolongación natural del desarrollo habitual en Ada. No hace falta aprender de nuevo una sintaxis especial.

3. Instalación de GNATprove y la primera demostración

Primero preparamos el entorno para ejecutar GNATprove.

Instalar Alire

GNATprove se distribuye junto con la cadena de herramientas GNAT. La forma más sencilla de obtenerla es Alire, un gestor de paquetes basado en fuentes para Ada/SPARK cuyo comando se llama alr. Los paquetes se obtienen desde la página de versiones del repositorio de Alire en GitHub.

Una vez instalado, elija el compilador por defecto.

alr toolchain --select

Se inicia un asistente de selección que muestra la lista de versiones de GNAT disponibles para instalar y permite elegir el compilador por defecto. Ejecutar alr toolchain sin argumentos muestra los compiladores ya instalados y cuál es el actual por defecto.

Comprobar la versión

Con el entorno ya preparado, anote la versión. El resultado de la demostración depende de la versión del demostrador. Es el primer dato que hay que comprobar si más adelante «un código que antes se demostraba deja de demostrarse».

alr version
gnatprove --version

Crear un proyecto

Con Alire, se puede crear un proyecto compatible con SPARK con el siguiente comando.

alr init --bin spark_demo
cd spark_demo

Como GNATprove se distribuye junto con el compilador GNAT, en cualquier entorno donde alr build compile correctamente ya se puede usar directamente el comando gnatprove.

Como primer objeto de demostración, escribamos una función que devuelva el valor absoluto.

package Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer
     with Post => Abs_Value'Result >= 0;

end Simple_Proof;

package body Simple_Proof with SPARK_Mode is

   function Abs_Value (X : Integer) return Integer is
   begin
      if X < 0 then
         return -X;
      else
         return X;
      end if;
   end Abs_Value;

end Simple_Proof;

Los puntos a destacar son los siguientes.

Se añade with SPARK_Mode tanto en la especificación como en el cuerpo del paquete
El Post declara la propiedad «el resultado es mayor o igual que 0»
El atributo 'Result se usa para referirse al valor devuelto por la función

Ejecutemos GNATprove sobre este código.

gnatprove -P spark_demo.gpr

El resultado es el siguiente.

SUMMARY
-------
Phase 1 of 2: generation of Global contracts ...
Phase 2 of 2: flow analysis and proof ...
simple_proof.adb:5:15: info: range check proved
simple_proof.adb:6:16: info: range check proved
simple_proof.ads:3:19: info: postcondition proved

El mensaje postcondition proved significa que se ha demostrado que, para todas las entradas Integer, el valor devuelto es mayor o igual que 0.

Esta experiencia es la puerta de entrada a SPARK.

La salida cuando no se puede demostrar

Fijarse solo en la salida de un caso exitoso no basta: en la práctica hace falta saber leer también la salida de un caso fallido. GNATprove informa de las comprobaciones que no ha podido demostrar indicando su posición en el código fuente. La forma básica es esta línea:

file.adb:12:37: medium: divide by zero might fail

Se refiere a la línea 12, columna 37 de file.adb, es decir, a la posición del operador de división /, y significa que «no se ha podido demostrar que el divisor no sea cero». Lo importante aquí es que dice might fail (podría fallar), no will fail (fallará). No siempre hay realmente un error. En la mayoría de los casos, simplemente falta información para que el demostrador pueda decidir.

Cuando se obtiene un contraejemplo, el informe es más detallado.

high: assertion might fail
--> counterex.adb:11:25
 11 |    pragma Assert (R < 42);
    |                  ^~~~~~
  + e.g. when R = 42
  + provers gave up before completing the proof

e.g. when R = 42 es el contraejemplo: indica de forma concreta que «no se cumple cuando R vale 42». Cuando GNATprove deduce que la causa es un contrato incompleto, a veces incluso sugiere una corrección.

possible fix: subprogram at line xxx should mention Var in a precondition
possible fix: loop at line xxx should mention Var in a loop invariant
possible fix: call at line xxx should mention Var in a postcondition

La forma más rápida de acostumbrarse a este tipo de mensajes es provocarlos deliberadamente. Por ejemplo, si en el Abs_Value anterior se cambia el Post a Abs_Value'Result > 0 (mayor que 0), aparece postcondition might fail porque no se puede demostrar el caso X = 0. Y si se quita el Pre de Increment, que veremos en el capítulo 5, aparece overflow check might fail. Alternar casos que tienen éxito con casos que fallan es el camino más rápido para acostumbrarse a GNATprove.

La gravedad de los mensajes (info / medium / high) y el catálogo de tipos de comprobación se organizan en el capítulo 12.

4. Fundamentos del diseño por contrato ── cómo escribir Pre y Post

La demostración en SPARK empieza por escribir contratos.

Los contratos son una característica del lenguaje de Ada 2012, pero en SPARK se convierten en la entrada de la demostración.

procedure Transfer (From, To : in out Account; Amount : Positive)
  with Pre  => From.Balance >= Amount,
       Post => From.Balance = From.Balance'Old - Amount
                and then
                To.Balance = To.Balance'Old + Amount;

Organicemos los criterios de diseño de Pre y Post.

Pre (precondición):
  Responsabilidad de quien llama
  «Si se llama cumpliendo esta condición, se garantiza el Post»
  Suficientemente débil (dentro de lo que la parte llamante puede cumplir) y a la vez tan fuerte como sea necesario

Post (poscondición):
  Responsabilidad de la implementación
  «Así queda el estado del mundo después de la llamada»
  El atributo 'Old permite referirse al valor anterior a la llamada
  Si es demasiado fuerte, la implementación queda demasiado limitada; si es demasiado débil, no se puede demostrar ninguna propiedad útil

También conviene tener presentes los errores habituales y cómo evitarlos.

Error 1: el Pre es demasiado fuerte
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → compruebe si la parte llamante siempre puede cumplir esa condición
  → no restrinja el Pre en exceso solo porque las pruebas pasen

Error 2: el Post es demasiado débil
  Post => True
  → no garantiza nada. La demostración pierde sentido

Error 3: olvidar un efecto secundario en el Post
  Post => Result = X * 2  (se pasa por alto la actualización de una variable global)
  → los efectos secundarios se declaran con contratos Global/Depends (capítulo 8)

5. Demostración de ausencia de desbordamiento ── garantizar la seguridad del cálculo numérico

Una de las demostraciones de SPARK con mayor beneficio práctico es la prevención de desbordamientos.

Observe el siguiente código.

procedure Increment (X : in out Integer)
  with SPARK_Mode,
       Pre  => X < Integer'Last,
       Post => X = X'Old + 1;

La clave es Pre => X < Integer'Last. Con este contrato, GNATprove puede demostrar que la suma no desborda.

Sin el contrato, GNATprove advierte de la posibilidad de desbordamiento.

medium: overflow check might fail

Lo mismo ocurre con cálculos más complejos.

function Average (A, B : Integer) return Integer
  with SPARK_Mode,
       Pre  => (if A >= 0 and B >= 0 then A <= Integer'Last - B
                elsif A < 0 and B < 0 then A >= Integer'First - B),
       Post => (if A <= B then A <= Average'Result and Average'Result <= B
                else B <= Average'Result and Average'Result <= A);

El Pre parece complicado, pero no es más que la condición «la suma de A y B no desborda», expresada por casos según el signo.

Idea clave:
  la esencia de demostrar la ausencia de desbordamiento es declarar en el Pre,
  antes de una suma o multiplicación, que «el resultado cabe en el rango del tipo»
  parece tedioso, pero una vez escrito no volverá a sufrir errores de desbordamiento

6. Invariantes de bucle ── demostrar propiedades de los bucles

Una de las partes más difíciles de la verificación formal es la demostración de bucles.

Como un bucle se ejecuta un número arbitrario de veces, las pruebas no pueden cubrir todos los casos. En SPARK se demuestra usando invariantes de bucle (Loop Invariant).

function Sum_Of_Naturals (N : Natural) return Natural
  with SPARK_Mode,
       Post => Sum_Of_Naturals'Result = (N * (N + 1)) / 2;

function Sum_Of_Naturals (N : Natural) return Natural is
   Result : Natural := 0;
begin
   for I in 1 .. N loop
      Result := Result + I;
      pragma Loop_Invariant (Result = (I * (I + 1)) / 2);
   end loop;
   return Result;
end Sum_Of_Naturals;

Diseñar un invariante de bucle requiere el siguiente razonamiento.

1. Escriba una propiedad que se cumpla al inicio de cada iteración del bucle
2. Elija una que, tras la última iteración, permita deducir el Post buscado
3. El invariante debe expresar en forma de fórmula el resultado parcial del cálculo hasta ese punto

Veamos también un ejemplo de búsqueda en un arreglo.

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural
  with SPARK_Mode,
       Post => (if Find'Result = 0 then
                  (for all K in Arr'Range => Arr (K) /= Target)
                else
                  Arr (Find'Result) = Target);

function Find (Arr : Array_Of_Integer; Target : Integer) return Natural is
begin
   for I in Arr'Range loop
      if Arr (I) = Target then
         return I;
      end if;
      pragma Loop_Invariant
        (for all K in Arr'First .. I => Arr (K) /= Target);
   end loop;
   return 0;
end Find;

Aquí el invariante dice: «en el rango explorado hasta ahora, Target no está presente».

Principios para diseñar invariantes de bucle:
  exprese en forma de fórmula «qué se puede afirmar tras haber recorrido el bucle n veces»
  en bucles sobre arreglos, es habitual la forma «en el rango ya procesado se cumple tal cosa»
  si el invariante es demasiado fuerte, no se puede demostrar; si es demasiado débil, no permite deducir el Post
  encontrar este equilibrio es donde se ve la habilidad al demostrar bucles

7. La pragma Assert ── propiedades parciales escritas dentro del código

Además de los contratos (Pre/Post), en SPARK se pueden escribir aserciones (Assert) en mitad del código.

procedure Divide (A, B : Integer; Q, R : out Integer)
  with SPARK_Mode,
       Pre  => B /= 0,
       Post => A = Q * B + R and R >= 0 and R < abs (B);

procedure Divide (A, B : Integer; Q, R : out Integer) is
begin
   Q := A / B;
   R := A rem B;

   pragma Assert (A = Q * B + R);
   pragma Assert (R >= 0);
   pragma Assert (R < abs (B));
end Divide;

Organicemos cuándo usar cada pragma.

Pre/Post:       la promesa a la entrada y a la salida del subprograma
Assert:         una propiedad que debe cumplirse en un punto concreto del código
Loop_Invariant: una propiedad que se mantiene en cada iteración del bucle
Loop_Variant:   la cantidad decreciente que demuestra que el bucle siempre termina

Los usos habituales de Assert son estos.

Confirmar resultados intermedios de un cálculo complejo
Confirmar el estado tras una bifurcación if/else
Confirmar propiedades del valor devuelto tras llamar a un procedimiento
Aportar un lema para demostraciones posteriores

8. Contratos de flujo de datos ── Global y Depends

Una de las funciones más potentes de SPARK son los contratos de flujo de datos.

Declaran explícitamente qué variables globales lee o escribe un subprograma.

package Counter_Unit with SPARK_Mode is

   Count : Natural := 0;

   procedure Increment
     with Global => (In_Out => Count);

   procedure Reset
     with Global => (Output => Count);

   function Get_Value return Natural
     with Global => (Input => Count);

end Counter_Unit;

El contrato Global tiene estos tres modos.

Input:  solo lectura (para funciones)
Output: solo escritura (para inicialización)
In_Out: lectura y escritura (para actualizaciones)

Además, la relación de dependencia entre variables se puede expresar con Depends.

procedure Transfer
  (From, To : in out Account)
  with Global => (Input => Exchange_Rate),
       Depends => (From =>+ (From, Exchange_Rate),
                   To   =>+ (To, Exchange_Rate));

=>+ significa «además del valor anterior, también depende de estas entradas».

Ventajas de los contratos de flujo de datos:
  1. se ve de un vistazo «qué toca esta función»
  2. los efectos secundarios no intencionados se detectan en tiempo de compilación
  3. sirven de entrada para el análisis del flujo de información de las variables
  4. ayudan a visualizar el flujo de datos en sistemas de gran tamaño

9. Niveles de demostración ── aplicación progresiva de Stone a Platinum

SPARK tiene el concepto de nivel de demostración (Proof Level).

Intentar demostrar todo el código por completo de una vez suele llevar al abandono. Por eso SPARK ofrece una estrategia de ir subiendo el rigor de la demostración por etapas.

Stone:
  confirma que el código es una versión válida del subconjunto SPARK
  se usa como etapa intermedia de la introducción

Bronze:
  Stone + demuestra que no se leen variables sin inicializar
  y que el flujo de datos es el previsto
  se aplica al mayor alcance posible

Silver:
  Bronze + demuestra que no se producen errores en tiempo de ejecución
  (fuera de rango, desbordamiento, división por cero) (AoRTE: Absence of Run-time Errors)
  el objetivo por defecto para software crítico

Gold:
  Silver + demuestra propiedades clave de integridad
  (propiedades esenciales de seguridad funcional o de seguridad informática)
  se aplica solo a la parte del código que tiene esas propiedades

Platinum:
  demuestra la corrección funcional completa respecto a la especificación de requisitos
  se aplica solo a las partes con el nivel de exigencia más alto
  tiene un coste elevado y hay pocos casos que lo alcancen

Lo que indica la palabra «nivel» ── --mode y --level son cosas distintas

Conviene aclarar aquí un punto que se confunde con facilidad. De Stone a Platinum son niveles de garantía del software, un concepto distinto de la opción --level de gnatprove. A lo primero le corresponde, en realidad, la opción --mode.

Silver, Gold y Platinum se activan con el mismo interruptor. La diferencia no está en cómo se ejecuta la herramienta, sino en hasta dónde se define el objetivo de verificación.

Por otro lado, --level=0 a --level=4 son ajustes preestablecidos que determinan cuánto esfuerzo dedicar a la demostración. Cuanto más alto el valor, más tiempo tarda, pero mayor es la capacidad de demostración. Por dentro es una combinación de interruptores individuales, como se muestra a continuación.

En resumen, --mode decide «qué se verifica» y --level decide «cuánto se insiste». Lo primero que hay que tener presente es --mode; considere --level como el mando que se sube cuando la demostración no pasa.

Hay otra advertencia práctica. Como --level se controla mediante un tiempo límite, el resultado depende del rendimiento y la carga de la máquina, y no es reproducible. Para entornos de CI o para compartir resultados entre varias personas, la documentación oficial recomienda usar --steps, que fija el límite en número de pasos de inferencia en lugar de tiempo, o --replay, que reproduce un resultado de demostración ya existente.

Fuente: SPARK User’s Guide (8.1 Levels of Software Assurance, y Appendix A Command Line Invocation)

La estrategia práctica de introducción queda así.

Etapa 1: pasar todo el proyecto por el nivel Stone
  → detectar errores de escritura en los contratos

Etapa 2: llevar los módulos importantes al nivel Silver
  → eliminar accesos fuera de rango y desbordamientos
  → aquí se evita ya buena parte de los errores reales en la práctica

Etapa 3: llevar la lógica central al nivel Gold
  → garantizar matemáticamente las propiedades clave de seguridad funcional y de seguridad informática
  → no todo el código, solo la parte que tiene esas propiedades

Etapa 4: solo las partes con el requisito más alto llegan a Platinum
  → demostrar la corrección funcional completa respecto a la especificación de requisitos
  → como el coste es alto, el alcance se reduce al mínimo

10. El flujo práctico de la demostración ── un flujo de trabajo que reduce los retrocesos

Presentamos un flujo de trabajo para usar GNATprove en el día a día.

1. Diseñar los tipos y la especificación
   decidir las restricciones de rango y los invariantes de tipo

2. Escribir los contratos (Pre/Post)
   expresar la especificación como contrato antes de implementar

3. Conseguir que compile
   resolver los errores de compilación con GNAT

4. Ejecutar GNATprove en el nivel Stone
   gnatprove -P proj.gpr --mode=stone

5. Revisar los avisos y corregir los contratos si hace falta
   prestar especial atención a las inicializaciones olvidadas
   si solo interesan la inicialización y el flujo de datos, use Bronze
   gnatprove -P proj.gpr --mode=bronze

6. Apuntar al nivel Silver
   gnatprove -P proj.gpr --mode=silver
   eliminar los errores en tiempo de ejecución

7. Si hay bucles, añadir invariantes
   si no se puede demostrar, comprobar si falta algún invariante

8. Demostrar las propiedades importantes en el nivel Gold
   gnatprove -P proj.gpr --mode=gold
   el interruptor de arranque es el mismo que en Silver; lo que cambia es el objetivo de verificación
   suba --level solo cuando la demostración no termine a tiempo
   ejemplo: gnatprove -P proj.gpr --mode=gold --level=3

Estos son los casos habituales de «no se puede demostrar» y cómo tratarlos.

Caso 1: «medium: postcondition might fail»
  → el Post es demasiado fuerte o el Pre es demasiado débil
  → o falta un invariante de bucle

Caso 2: «medium: overflow check might fail»
  → limite el rango de valores en el Pre
  → o estreche el rango del propio tipo

Caso 3: «medium: array index check might fail»
  → demuestre con un invariante que el rango del bucle está dentro del rango del arreglo
  → use for I in Arr'Range (ayuda a que SPARK reconozca el rango automáticamente)

Caso 4: «prover timeout»
  → el demostrador ha agotado el tiempo. Divida la demostración por etapas con invariantes
  → o divida la función en partes más pequeñas

11. Uso combinado de SPARK y las pruebas ── entender la relación de complementariedad

La verificación formal y las pruebas no se oponen: se complementan.

La demostración de SPARK:
  se cumple para todas las entradas posibles
  solo cubre las propiedades escritas en el contrato
  en los casos que no se pueden demostrar, se recurre a la revisión manual o a las pruebas

Las pruebas:
  confirman el comportamiento real para las entradas seleccionadas
  también pueden descubrir supuestos implícitos que no están en el contrato
  permiten confirmar la interacción con el entorno de ejecución

El patrón de uso combinado es este.

1. Garantizar con SPARK el nivel Silver (sin errores en tiempo de ejecución)
2. Confirmar con pruebas unitarias la corrección de entradas y salidas concretas
3. Demostrar la lógica central en el nivel Gold
4. Concentrar las pruebas en las partes que no se pueden demostrar

Ada cuenta con un framework de pruebas unitarias llamado AUnit. En la práctica resulta útil combinar SPARK para fijar tipos y contratos con AUnit para probar el comportamiento.

12. Cómo leer los resultados de GNATprove ── interpretación de los mensajes

La salida de GNATprove tiene estos tres niveles.

info:    demostración exitosa
medium:  demostración fallida (advertencia). Requiere revisión manual
high:    demostración fallida (error). Probable violación del contrato

Estos son los mensajes habituales y su significado.

«postcondition proved»           se ha demostrado la poscondición
«range check proved»             se ha demostrado la comprobación de rango
«overflow check proved»          se ha demostrado que no hay desbordamiento
«index check proved»             se ha demostrado el rango del índice del arreglo
«divide by zero check proved»    se ha demostrado que no se produce división por cero

«might fail»                     no se pudo demostrar
«cannot prove»                   el demostrador no pudo completar la demostración
«prover timeout»                 la demostración no terminó dentro del tiempo límite

Estos son los pasos a seguir cuando aparece might fail.

1. Juzgar leyendo el código si realmente puede fallar
2. Si puede fallar, corregir el código
3. Si no debería fallar, reforzar el contrato (Pre/invariante)
4. Si aun así no se puede demostrar, declararlo como supuesto con pragma Assume
   (aunque Assume es un supuesto sin demostrar, así que hay que usarlo con cuidado)

13. Cómo incorporarlo en un proyecto real

Un enfoque realista para introducir SPARK en un proyecto existente.

1. Empezar por el código nuevo
   no intente convertir a SPARK todo el código existente de una vez
   active SPARK_Mode en los módulos que empiece a escribir desde cero

2. Ponerse como objetivo Silver
   Gold (demostración de propiedades clave de integridad) o Platinum (demostración funcional completa)
   son ideales, pero empiece por Silver (sin errores en tiempo de ejecución)
   solo con la prevención de desbordamientos ya se obtiene un valor práctico muy alto

3. Escribir los contratos a partir de la interfaz
   escriba los contratos en la especificación del paquete (.ads) antes que la implementación
   con la especificación ya fijada, cualquier implementador puede escribir código que cumpla el contrato

4. Incorporarlo a CI/CD
   añada gnatprove al pipeline de integración continua
   detenga la compilación (o emita un aviso) si falla una demostración

5. Acumular informes de demostración
   genere un informe con gnatprove --report=all
   siga la evolución de los elementos aún no demostrados

En proyectos con código C/C++ existente mezclado, resulta útil el siguiente enfoque progresivo.

1. Escribir los módulos nuevos en Ada/SPARK
2. Conectar con C/C++ mediante Interfaces.C
3. Migrar a SPARK las estructuras de datos y la lógica de verificación importantes
4. Ampliar progresivamente el alcance de SPARK

14. Límites y precauciones de SPARK

SPARK tampoco es omnipotente. Entender honestamente sus límites es la base de una aplicación correcta.

Alcance de lo que se puede demostrar:
  SPARK solo demuestra «las propiedades escritas en el contrato»
  las lagunas del contrato (propiedades que se olvidó escribir) no se demuestran
  ejemplo: aunque el Post demuestre que el resultado está ordenado, si se olvida escribir
  «no es destructivo», no queda garantizado que se conserven los elementos originales

Límites de los demostradores:
  hay propiedades complejas que los demostradores automáticos no pueden demostrar
  en esos casos hace falta recurrir a la demostración manual (por ejemplo, con Coq)
  aun así, en el ámbito práctico la demostración automática suele bastar

Restricciones del lenguaje:
  el código que usa punteros de forma intensiva no se puede convertir a SPARK
  la demostración de la asignación dinámica de memoria es limitada
  demostrar estructuras de datos recursivas es difícil

Formación del desarrollador:
  escribir contratos requiere entrenamiento
  diseñar invariantes de bucle es, en particular, algo que lleva tiempo dominar
  es indispensable un plan de formación para todo el equipo

15. Resumen ── llevar la demostración al desarrollo diario

Hemos repasado la práctica de la verificación formal con SPARK.

SPARK es un subconjunto de Ada limitado a funciones demostrables
los contratos (Pre/Post) son la entrada de la demostración. Se puede usar directamente el contrato de Ada 2012
GNATprove ejecuta la demostración automática e informa del resultado a nivel de código fuente
los invariantes de bucle demuestran propiedades de los bucles
Global/Depends declara el flujo de datos de forma explícita y gestiona los efectos secundarios
los niveles de demostración (Stone a Platinum) permiten subir el rigor por etapas
lo práctico es apuntar primero al nivel Silver (sin errores en tiempo de ejecución)
las pruebas y la demostración no se oponen: se complementan

Puede que tenga la idea preconcebida de que «la verificación formal es difícil y solo es para proyectos especiales».

Pero hoy en día la combinación de SPARK y GNATprove ha llegado al siguiente nivel.

1. Escribir el contrato. Es, en esencia, el mismo trabajo de diseño que escribir tipos o pruebas
2. Ejecutar gnatprove. Se siente igual que compilar
3. Ver el resultado y corregir el código o el contrato

Este ciclo no es distinto del flujo de desarrollo diario de corregir el código mientras se leen los mensajes de error del compilador.

La diferencia es que el compilador garantiza que «la sintaxis es correcta», mientras que GNATprove garantiza que «es correcto para todas las entradas».

El eslogan de Ada que presentamos en el artículo anterior, «los errores no se buscan: se hacen imposibles de escribir mediante los tipos y los contratos», avanza un paso más gracias a SPARK.

La ausencia de errores se garantiza mediante la demostración.

Pruebe primero a añadir SPARK_Mode y Post a una función pequeña, y ejecute gnatprove.

Cuando vea el mensaje en verde postcondition proved, su forma de ver la garantía de calidad del software habrá cambiado.

Referencias

• Colección de referencia con los fragmentos de código de este artículo, organizados por capítulos - komurasoft-blog-samples (GitHub)
• SPARK - AdaCore
• Introduction to SPARK - learn.adacore.com
• SPARK 2014 Reference Manual
• GNATprove User’s Guide
• Ada Reference Manual (Ada 2022)
• Alire - Ada Library Repository
• Why3 - Platform for Deductive Program Verification
• El atractivo del lenguaje Ada ── un lenguaje que expresa el diseño mediante tipos y sostiene software en funcionamiento durante décadas - este sitio

Artículos relacionados

Artículos recientes con las mismas etiquetas para profundizar en temas cercanos.

Temas relacionados

Estas páginas sitúan el tema en un contexto más amplio de servicios y decisiones.

Preguntas frecuentes

Preguntas habituales en las consultas sobre el tema del artículo.

¿Qué es SPARK y qué relación tiene con Ada?

SPARK es un subconjunto (lenguaje parcial) de Ada, diseñado para poder demostrar matemáticamente las propiedades de un programa. A cambio de restringir la gestión dinámica de memoria mediante punteros y el uso libre de excepciones, entre otras características, obtiene la posibilidad de demostración. El código SPARK es código Ada con anotaciones de contrato añadidas, por lo que se sitúa en la prolongación natural del desarrollo habitual en Ada y no exige aprender una sintaxis especial nueva. La herramienta central es GNATprove, proporcionada por AdaCore, que convierte los contratos al lenguaje intermedio Why3 e intenta demostrarlos con probadores automáticos como Z3.

¿En qué se diferencia la verificación formal de las pruebas?

Las pruebas confirman que el programa «funciona correctamente para las entradas seleccionadas», mientras que la verificación formal demuestra matemáticamente que «una propiedad se cumple para todas las entradas posibles». Como las combinaciones de entradas son infinitas, las pruebas por sí solas no pueden demostrar la corrección para todas ellas. Sin embargo, ambos enfoques no son opuestos, sino complementarios: en la práctica resulta útil garantizar con SPARK el nivel Silver (ausencia de errores en tiempo de ejecución), confirmar con pruebas unitarias entradas y salidas concretas, y concentrar las pruebas en las partes que no se pueden demostrar.

¿Qué son los niveles de demostración de SPARK (Stone a Platinum)?

Es un concepto para elevar progresivamente el rigor de la demostración. Stone confirma que el código es SPARK válido; Bronze demuestra que no se leen variables sin inicializar y que el flujo de datos es correcto; Silver demuestra que no se producen errores en tiempo de ejecución (fuera de rango, desbordamiento, división por cero). Gold añade a lo anterior la demostración de propiedades clave de integridad, como que se mantienen invariantes de datos importantes o que las transiciones de estado siguen la especificación. Platinum es el nivel de corrección funcional completa, en el que los contratos cubren todos los requisitos funcionales y se demuestra que la implementación se ajusta a la especificación; tiene un coste elevado y son pocos los proyectos que lo alcanzan. En la práctica, el objetivo más realista es apuntar primero al nivel Silver.

¿Qué hacer cuando GNATprove no logra demostrar algo?

La respuesta depende del mensaje. «postcondition might fail» suele deberse a una poscondición demasiado fuerte, una precondición demasiado débil o un invariante de bucle insuficiente. «overflow check might fail» se resuelve limitando el rango de valores en la precondición o estrechando el rango del propio tipo. «array index check might fail» se resuelve demostrando con un invariante que el rango del bucle está dentro del rango del arreglo. «prover timeout» se resuelve dividiendo la demostración en pasos mediante invariantes o dividiendo la función en piezas más pequeñas. El primer paso siempre es leer el código y juzgar si realmente puede fallar.

Perfil del autor

Página de presentación del autor del artículo.

Go Komura

Representante de KomuraSoft LLC

Especializado en desarrollo de software para Windows, consultoría técnica e investigación de fallos, sobre todo en proyectos con sistemas existentes y errores difíciles de reproducir.