KomuraSoft LLC
Contáctenos
Menú

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

· · Ada, SPARK, Verificación Formal, GNATprove, Diseño por Contrato, Alta Integridad, Lenguaje de Programación, Alta Fiabilidad

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 inherentes. El número de entradas posibles es infinito, y las pruebas por sí solas no pueden demostrar la corrección 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», ofreció una visión general de Ada y mencionó SPARK brevemente.

Este artículo se centra específicamente en la verificación formal práctica con SPARK y aborda lo siguiente:

Qué es SPARK y su relación con Ada
Cómo escribir contratos (Pre/Post)
Cómo demostrarlos con GNATprove
Cómo diseñar invariantes de bucle
Cómo gestionar los efectos secundarios con contratos de flujo de datos (Global/Depends)
Una estrategia de adopción gradual mediante niveles de demostración (de Stone a Platinum)
Cómo integrar SPARK en proyectos reales

El objetivo es que experimente el paso de las pruebas a la demostración a través de ejemplos de código reales.

Los fragmentos de código de este artículo están disponibles, organizados por capítulo, como colección de referencia en GitHub.

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

2. Qué es SPARK ── El subconjunto de Ada como puerta de entrada al mundo de la demostración

SPARK es un subconjunto del lenguaje Ada.

Ser un subconjunto es una decisión de diseño deliberada.

Ada completo → muy expresivo, pero verificarlo por completo no es realista
SPARK        → restringido a características verificables, lo que hace realista la demostración

Las principales restricciones que impone SPARK son:

Gestión dinámica de memoria mediante punteros (tipos access) → controlada por un modelo de propiedad
Uso libre de manejadores de excepciones                       → permitido de forma restringida
Estructuras de datos recursivas                                → restringidas por ser difíciles de demostrar
Uso libre de tareas (tasking)                                   → restringido mediante el perfil Ravenscar

La palabra «restricciones» puede sonar limitante, pero estas restricciones son el precio de la demostrabilidad.

El núcleo del conjunto de herramientas de SPARK es GNATprove, proporcionado por AdaCore.

Cómo funciona GNATprove:
1. Analiza código Ada anotado con SPARK
2. Traduce los contratos (Pre/Post) y las aserciones al lenguaje intermedio Why3
3. Intenta demostraciones con probadores automáticos como Z3, CVC4 y Alt-Ergo
4. Informa los resultados como mensajes directamente sobre el código fuente

Un punto crucial: SPARK está construido sobre Ada.

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

Dicho de otro modo, SPARK es una extensión natural del desarrollo cotidiano en Ada. No hace falta aprender una sintaxis completamente nueva.

3. Instalar GNATprove y la primera demostración

Primero, preparemos un entorno para ejecutar GNATprove.

Con Alire se puede crear un proyecto listo para SPARK con el siguiente comando:

alr init --bin spark_demo
cd spark_demo

Como GNATprove viene incluido con el compilador GNAT, el comando gnatprove está disponible en cuanto el proyecto compila con alr build.

Como primer objetivo 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;

Puntos clave a observar:

with SPARK_Mode se añade tanto a la especificación del paquete como al cuerpo
La condición Post declara la propiedad «el resultado es no negativo»
El atributo 'Result permite referirse al valor de retorno de la función

Ahora ejecutemos GNATprove sobre este código:

gnatprove -P spark_demo.gpr

El resultado será similar a este:

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 matemáticamente que, para todas las entradas Integer posibles, el valor de retorno es no negativo.

Esta es la experiencia de entrada a SPARK.

4. Fundamentos del diseño por contrato ── Escribir Pre y Post

Las demostraciones de SPARK comienzan escribiendo contratos.

Los contratos son una característica del lenguaje 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;

Directrices para diseñar Pre y Post:

Pre (precondición):
  Responsabilidad de quien llama
  «Si me llamas cumpliendo esta condición, garantizo la Post»
  Lo bastante débil para ser satisfacible, lo bastante fuerte para ser útil

Post (poscondición):
  Responsabilidad de la implementación
  «Después de la llamada, el mundo está en este estado»
  El atributo 'Old permite referirse a los valores previos a la llamada
  Demasiado fuerte hace la implementación demasiado restrictiva; demasiado débil no demuestra nada útil

Errores comunes y cómo evitarlos:

Error 1: Pre demasiado fuerte
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → Comprobar: ¿puede quien llama satisfacer siempre esta condición?
  → No restringir Pre solo porque las pruebas pasen

Error 2: Post demasiado débil
  Post => True
  → No garantiza nada. La demostración carece de sentido.

Error 3: Olvidar los efectos secundarios en Post
  Post => Result = X * 2  (se pasa por alto la actualización de una variable global)
  → Hacer explícitos los efectos secundarios con contratos Global/Depends (sección 9)

5. Demostrar la ausencia de desbordamiento ── Garantizar la seguridad numérica

Una de las cosas más valiosas en la práctica que SPARK puede demostrar es la ausencia de desbordamiento (overflow).

Considere este código:

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

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

Sin contrato, GNATprove advierte de un posible desbordamiento:

medium: overflow check might fail

Lo mismo se aplica a 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);

La Pre parece compleja, pero simplemente expresa que «la suma A+B no se desborda», distinguiendo casos según el signo.

Idea clave:
  La esencia de la demostración de ausencia de desbordamiento consiste
  en declarar en Pre que el resultado de una suma o multiplicación cabe
  dentro del rango del tipo
  Puede parecer tedioso, pero una vez escrito, nunca más le atormentará
  un error 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.

Los bucles se ejecutan un número arbitrario de veces, por lo que las pruebas no pueden cubrir todos los casos. SPARK utiliza para ello los invariantes de bucle (Loop Invariants).

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 invariantes de bucle exige el siguiente planteamiento:

1. Escribir una propiedad que se cumpla al inicio de cada iteración
2. Elegir una que, tras la última iteración, implique la Post deseada
3. El invariante expresa como fórmula el cálculo parcial realizado hasta ese punto

He aquí otro ejemplo: la búsqueda en un array.

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;

El invariante aquí es: «en el rango examinado hasta ahora, Target no existe».

Principios para diseñar invariantes de bucle:
  Expresar como fórmula: «tras n iteraciones, ¿qué podemos afirmar?»
  En los bucles sobre arrays, el patrón habitual es «para el rango ya procesado, se cumple P»
  Un invariante demasiado fuerte no se puede demostrar; uno demasiado débil no implica la Post
  Encontrar el equilibrio adecuado es el verdadero arte de demostrar bucles

7. Pragmas de aserción ── Propiedades parciales dentro del código

Además de los contratos (Pre/Post), SPARK permite escribir aserciones (Assert) directamente en el cuerpo 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;

Uso de los distintos pragmas:

Pre/Post:       Promesas en la entrada y 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:   Una cantidad decreciente para demostrar que el bucle termina

Buenos casos de uso para Assert:

Verificar resultados intermedios de cálculos complejos
Comprobar el estado tras una rama if/else
Confirmar propiedades de los valores de retorno tras llamar a un procedimiento
Aportar lemas que faciliten demostraciones posteriores

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

Una de las características potentes de SPARK son los contratos de flujo de datos.

Declaran explícitamente qué variables globales lee y 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;

Los modos del contrato Global son:

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

Además, las dependencias entre variables pueden expresarse con Depends:

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

=>+ significa «depende del valor anterior más estas entradas adicionales».

Ventajas de los contratos de flujo de datos:
  1. «¿Qué toca esta función?» se ve de un vistazo
  2. Los efectos secundarios no intencionados se detectan en tiempo de compilación
  3. Alimentan el análisis de flujo de información de las variables
  4. Ayudan a visualizar el flujo de datos en sistemas grandes

9. Niveles de demostración ── Adopción gradual de Stone a Platinum

SPARK define el concepto de niveles de demostración (Proof Levels).

Intentar demostrar por completo todo el código de una vez suele llevar a la frustración. Por eso SPARK ofrece una estrategia para aumentar el rigor de la demostración de forma gradual.

Stone (nivel 0):
  Solo verificación de la sintaxis de los contratos y la consistencia de tipos
  El primer nivel que hay que alcanzar

Bronze (nivel 1):
  Stone + demostración de ausencia de lecturas de variables no inicializadas
  Garantía de corrección básica

Silver (nivel 2):
  Bronze + demostración de ausencia de errores en tiempo de ejecución
  (fuera de rango, desbordamiento, división por cero)
  El objetivo más pragmático

Gold (nivel 3):
  Silver + demostración de las condiciones Pre/Post
  Garantía de corrección funcional completa

Platinum (nivel 4):
  Gold + demostración de la no interferencia de datos y el flujo de
  información
  Para sistemas orientados a la seguridad

Una estrategia de adopción práctica:

Fase 1: llevar todo el proyecto al nivel Stone
  → Detectar errores al escribir los contratos

Fase 2: llevar los módulos críticos al nivel Silver
  → Eliminar desbordamientos y accesos fuera de rango
  → La mayoría de los errores reales se evitan aquí

Fase 3: demostrar la lógica central al nivel Gold
  → Garantizar matemáticamente la corrección funcional
  → Demostrar la corrección de los algoritmos

Fase 4: pasar a Platinum si hay requisitos de seguridad
  → Detectar rutas de fuga de información

10. Un flujo de trabajo práctico de demostración ── Reducir el retrabajo

Aquí tiene un flujo de trabajo para usar GNATprove en el día a día:

1. Diseñar los tipos y las especificaciones
   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
   Corregir los errores de compilación con GNAT

4. Ejecutar GNATprove en el nivel Stone
   gnatprove -P proj.gpr --level=0

5. Revisar las advertencias y refinar los contratos si es necesario
   Prestar especial atención a los problemas de inicialización

6. Buscar el nivel Silver
   gnatprove -P proj.gpr --level=2
   Eliminar todos los errores en tiempo de ejecución

7. Añadir invariantes de bucle donde sea necesario
   Si una demostración falla, comprobar si faltan invariantes

8. Demostrar la corrección funcional en el nivel Gold
   gnatprove -P proj.gpr --level=3

Casos comunes de «no se puede demostrar» y cómo abordarlos:

Caso 1: «medium: postcondition might fail»
  → Post demasiado fuerte, o Pre demasiado débil
  → O invariantes de bucle insuficientes

Caso 2: «medium: overflow check might fail»
  → Restringir los rangos de valores en Pre
  → O reducir el rango del propio tipo

Caso 3: «medium: array index check might fail»
  → Usar un invariante de bucle para mostrar que el rango del bucle
    está dentro de los límites del array
  → Usar for I in Arr'Range para ayudar al reconocimiento automático
    de rangos de SPARK

Caso 4: «prover timeout»
  → El probador ha agotado el tiempo; dividir con invariantes graduales
  → Dividir las funciones grandes en funciones más pequeñas

11. Usar SPARK y las pruebas juntos ── Entender la relación complementaria

La verificación formal y las pruebas no son adversarias; se complementan.

Demostraciones de SPARK:
  Demuestran propiedades para todas las entradas posibles
  Solo cubren las propiedades escritas en los contratos
  Los casos no demostrables se dejan a la revisión manual o a las pruebas

Pruebas:
  Verifican el comportamiento real para las entradas seleccionadas
  Pueden descubrir supuestos implícitos no escritos en los contratos
  Pueden verificar la interacción con el entorno de ejecución

Patrones de uso combinado:

1. Garantizar la ausencia de errores en tiempo de ejecución (nivel
   Silver) con SPARK
2. Verificar la corrección concreta de entrada/salida con pruebas
   unitarias
3. Demostrar la lógica central en el nivel Gold
4. Concentrar las pruebas en las partes no demostrables

Ada dispone del framework de pruebas unitarias AUnit. Una combinación práctica consiste en consolidar tipos y contratos con SPARK y luego probar el comportamiento con AUnit.

12. Leer los resultados de GNATprove ── Interpretar los mensajes

La salida de GNATprove tiene tres niveles de gravedad:

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

Mensajes comunes y su significado:

«postcondition proved»          se ha demostrado la condición Post
«range check proved»            se ha demostrado la comprobación de rango
«overflow check proved»         se ha demostrado la ausencia de desbordamiento
«index check proved»            se han demostrado los límites del índice del array
«divide by zero check proved»   se ha demostrado la ausencia de división por cero

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

Procedimiento a seguir ante might fail:

1. Leer el código y juzgar 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 suposición con
   pragma Assume (atención: Assume es una suposición no demostrada,
   úsese con cautela)

13. Integración en proyectos reales

Un enfoque realista para introducir SPARK en un proyecto existente:

1. Empezar por el código nuevo
   No intentar convertir todo el código existente a SPARK de una vez
   Activar SPARK_Mode en los módulos recién escritos

2. Buscar Silver
   Gold (demostración funcional completa) es lo ideal, pero se empieza
   con Silver (sin errores en tiempo de ejecución)
   Incluso solo evitar el desbordamiento tiene un valor práctico enorme

3. Escribir los contratos partiendo de las interfaces
   Escribir los contratos en la especificación del paquete (.ads) antes
   de implementar
   Con una especificación sólida, cualquier implementador puede escribir
   código que satisfaga los contratos

4. Integrar en CI/CD
   Añadir gnatprove al pipeline de CI
   Detener la compilación (o al menos advertir) si falla una demostración

5. Acumular informes de demostración
   Generar informes con gnatprove --report=all
   Seguir la evolución de los elementos no demostrados con el tiempo

Para proyectos con código mixto de C/C++ y Ada, un enfoque gradual resulta eficaz:

1. Escribir los módulos nuevos en Ada/SPARK
2. Interactuar con C/C++ a través de Interfaces.C
3. Migrar a SPARK las estructuras de datos críticas y la lógica de
   verificación
4. Ampliar gradualmente la cobertura de SPARK

14. Límites y precauciones de SPARK

SPARK tampoco es una solución universal. Comprender honestamente sus límites conduce a una aplicación correcta.

Lo que SPARK puede demostrar:
  SPARK solo demuestra las propiedades escritas en los contratos
  Las propiedades omitidas (olvidadas al escribir) no se demuestran
  Ejemplo: demostrar en Post que el resultado está ordenado no garantiza
  que se preserven los elementos originales, a menos que eso también
  se escriba

Límites de los probadores:
  Algunas propiedades complejas superan lo que pueden manejar los
  probadores automáticos
  En esos casos hace falta demostración interactiva (Coq, etc.)
  Aun así, la demostración automática basta para la mayoría de los
  casos prácticos

Restricciones del lenguaje:
  El código con uso intensivo de punteros no se puede convertir a SPARK
  La demostración de la asignación dinámica de memoria es limitada
  La demostración de estructuras de datos recursivas es difícil

Dominio por parte de los desarrolladores:
  Escribir contratos requiere práctica
  Diseñar invariantes de bucle lleva especialmente tiempo aprenderlo
  Un plan de mejora de competencias para todo el equipo es indispensable

15. Conclusión ── Hacer de la demostración parte del desarrollo diario

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

SPARK es un subconjunto de Ada, restringido a características verificables
Los contratos (Pre/Post) son la entrada de las demostraciones. Los
contratos de Ada 2012 funcionan directamente
GNATprove ejecuta demostraciones automáticas e informa los resultados
a nivel de código fuente
Los invariantes de bucle demuestran propiedades de los bucles
Global/Depends hacen explícito el flujo de datos y gestionan los
efectos secundarios
Los niveles de demostración (de Stone a Platinum) permiten aumentar
el rigor por etapas
Buscar primero el nivel Silver (sin errores en tiempo de ejecución) es
la recomendación práctica
Las pruebas y las demostraciones no son opuestas: se complementan

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

Pero la combinación actual de SPARK y GNATprove ha alcanzado el siguiente nivel:

1. Escribir un contrato. Es fundamentalmente la misma actividad de
   diseño que escribir tipos o pruebas
2. Ejecutar gnatprove. Se siente como compilar
3. Mirar los resultados y corregir el código o el contrato

Este ciclo no es distinto del flujo de desarrollo diario en el que se corrige código leyendo los mensajes de error del compilador.

La diferencia es esta: mientras que un compilador garantiza que «la sintaxis es correcta», GNATprove garantiza «la corrección para todas las entradas».

El lema de Ada presentado en el artículo anterior —«los errores no se encuentran; los tipos y los contratos hacen imposible escribirlos»— avanza al siguiente nivel con SPARK:

La ausencia de errores está garantizada por la demostración.

Empiece añadiendo SPARK_Mode y un Post a una función pequeña, y luego ejecute gnatprove.

Cuando vea el mensaje verde postcondition proved, su forma de ver el aseguramiento de la calidad del software cambiará.

Referencias

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 de Ada deliberadamente restringido, diseñado para que las propiedades de un programa puedan demostrarse matemáticamente. Limita características difíciles de verificar —uso libre de punteros, manejo ilimitado de excepciones, estructuras de datos recursivas y tareas sin restricciones— a cambio de demostrabilidad. El código SPARK es código Ada más anotaciones de contrato, por lo que constituye una extensión natural del desarrollo cotidiano en Ada y no un lenguaje distinto; la herramienta GNATprove traduce los contratos al lenguaje intermedio Why3 e intenta demostraciones con probadores automáticos como Z3, CVC4 y Alt-Ergo.
¿En qué se diferencia la verificación formal con SPARK de las pruebas?
Las pruebas verifican que el programa se comporte correctamente para las entradas seleccionadas; la verificación formal demuestra matemáticamente que una propiedad se cumple para todas las entradas posibles. Ambas se complementan en lugar de competir: SPARK solo demuestra las propiedades escritas en los contratos, mientras que las pruebas pueden descubrir supuestos implícitos nunca formalizados y verificar la interacción con el entorno de ejecución. Una combinación práctica consiste en garantizar la ausencia de errores en tiempo de ejecución con SPARK, verificar comportamientos concretos de entrada/salida con pruebas unitarias y concentrar las pruebas en las partes que no se pueden demostrar.
¿Cuáles son los niveles de demostración de SPARK y cuál conviene buscar primero?
SPARK define cinco niveles de rigor creciente: Stone (sintaxis de los contratos y consistencia de tipos), Bronze (añade la demostración de ausencia de lecturas no inicializadas), Silver (añade la demostración de ausencia de errores en tiempo de ejecución como desbordamientos, violaciones de rango y división por cero), Gold (añade la demostración de corrección funcional mediante Pre/Post) y Platinum (añade la no interferencia de datos y el flujo de información). Silver es el objetivo inicial más pragmático —la mayoría de los errores reales se eliminan ya con la ausencia de errores en tiempo de ejecución— y Gold merece la pena para la lógica central cuya corrección deba garantizarse.
¿Qué es un invariante de bucle y por qué lo necesitan las demostraciones de SPARK?
Un invariante de bucle es una propiedad que se cumple al inicio de cada iteración, escrita con pragma Loop_Invariant. Los bucles se ejecutan un número arbitrario de veces, por lo que el probador necesita el invariante para razonar sobre todas las iteraciones a la vez: expresa como fórmula el cálculo parcial realizado hasta ese punto, y tras la última iteración debe implicar la poscondición deseada. Diseñar invariantes es la habilidad más delicada en las demostraciones de bucles: un invariante demasiado fuerte no se puede demostrar, y uno demasiado débil no implica la poscondición.

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.

Contactar
Volver al blog