KomuraSoft LLC
Nous contacter
Menu

Introduction à la vérification formelle avec SPARK ── Des contrats Ada à la preuve mathématique

· · Ada, SPARK, Vérification Formelle, GNATprove, Conception par Contrat, Haute Intégrité, Langage de Programmation, Haute Fiabilité

1. Introduction ── Au-delà de « exécuter et observer »

Le moyen le plus courant d’assurer la qualité d’un logiciel reste le test.

Test : vérifie que le programme se comporte correctement pour les entrées sélectionnées

Mais les tests ont des limites intrinsèques. Le nombre d’entrées possibles est infini, et les tests seuls ne peuvent pas démontrer la correction pour toutes.

C’est ici qu’intervient la vérification formelle (Formal Verification).

Vérification formelle : prouve mathématiquement qu'une propriété est vraie pour toutes les entrées possibles

L’article précédent, « L’attrait du langage Ada », donnait un aperçu d’Ada et abordait brièvement SPARK.

Cet article se concentre spécifiquement sur la vérification formelle pratique avec SPARK et couvre les points suivants :

Ce qu'est SPARK et son rapport avec Ada
Comment écrire des contrats (Pre/Post)
Comment les prouver avec GNATprove
Comment concevoir des invariants de boucle
Comment gérer les effets de bord avec les contrats de flux de données (Global/Depends)
Une stratégie d'adoption progressive via les niveaux de preuve (de Stone à Platinum)
Comment intégrer SPARK dans des projets réels

L’objectif est de vous faire vivre le passage du test à la preuve à travers des exemples de code concrets.

Les extraits de code de cet article sont disponibles, organisés par chapitre, dans un dépôt de référence sur GitHub.

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

2. Qu’est-ce que SPARK ── Le sous-ensemble d’Ada, porte d’entrée vers le monde de la preuve

SPARK est un sous-ensemble du langage Ada.

Le fait d’être un sous-ensemble relève d’un choix de conception délibéré.

Ada complet → très expressif, mais vérifier l'ensemble n'est pas réaliste
SPARK       → restreint aux fonctionnalités vérifiables, ce qui rend la preuve réaliste

Voici les principales restrictions imposées par SPARK :

Gestion dynamique de la mémoire via des pointeurs (types access) → contrôlée par un modèle de propriété
Usage libre des gestionnaires d'exceptions                       → autorisé sous forme restreinte
Structures de données récursives                                 → restreintes car difficiles à prouver
Usage libre des tâches                                            → restreint via le profil Ravenscar

Le mot « restrictions » peut sembler contraignant, mais ces restrictions sont le prix à payer pour la prouvabilité.

Le cœur de l’outillage SPARK est GNATprove, fourni par AdaCore.

Fonctionnement de GNATprove :
1. Analyse le code Ada annoté SPARK
2. Traduit les contrats (Pre/Post) et les assertions vers le langage intermédiaire Why3
3. Tente des preuves à l'aide de solveurs automatiques tels que Z3, CVC4 et Alt-Ergo
4. Rapporte les résultats sous forme de messages sur le code source

Un point crucial : SPARK est construit au-dessus d’Ada.

Code SPARK = code Ada + annotations de contrat

Autrement dit, SPARK prolonge naturellement le développement Ada quotidien. Il n’y a pas de syntaxe entièrement nouvelle à apprendre.

3. Installer GNATprove et réaliser sa première preuve

Commençons par mettre en place un environnement pour exécuter GNATprove.

Avec Alire, on peut créer un projet prêt pour SPARK avec la commande suivante :

alr init --bin spark_demo
cd spark_demo

GNATprove étant fourni avec le compilateur GNAT, la commande gnatprove est disponible dès lors que le projet se compile avec alr build.

Comme première cible de preuve, écrivons une fonction qui retourne la valeur absolue.

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;

Points essentiels à noter :

with SPARK_Mode s'ajoute à la fois à la spécification du package et à son corps
La condition Post déclare la propriété « le résultat est non négatif »
L'attribut 'Result permet de référencer la valeur de retour de la fonction

Exécutons maintenant GNATprove sur ce code :

gnatprove -P spark_demo.gpr

Le résultat ressemble à ceci :

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

Le message postcondition proved signifie que pour toutes les entrées Integer possibles, il a été mathématiquement prouvé que la valeur de retour est non négative.

C’est là l’expérience d’entrée dans SPARK.

4. Fondements de la conception par contrat ── Écrire Pre et Post

Les preuves SPARK commencent par l’écriture de contrats.

Les contrats sont une fonctionnalité du langage Ada 2012, mais dans SPARK, ils deviennent l’entrée de la preuve.

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;

Principes de conception pour Pre et Post :

Pre (précondition) :
  Responsabilité de l'appelant
  « Si vous m'appelez en satisfaisant cette condition, je garantis la Post »
  Assez faible pour être satisfiable, assez forte pour être utile

Post (postcondition) :
  Responsabilité de l'implémentation
  « Après l'appel, le monde est dans cet état »
  L'attribut 'Old permet de référencer les valeurs antérieures à l'appel
  Trop forte, l'implémentation devient trop contrainte ; trop faible, rien d'utile n'est prouvé

Erreurs fréquentes et comment les éviter :

Erreur 1 : Pre trop forte
  Pre => X > 0 and X < 100 and X /= 50 and ...
  → Vérifier : l'appelant peut-il toujours satisfaire cette condition ?
  → Ne pas resserrer Pre simplement parce que les tests passent

Erreur 2 : Post trop faible
  Post => True
  → Ne garantit rien. La preuve est vide de sens.

Erreur 3 : Oublier les effets de bord dans Post
  Post => Result = X * 2  (mise à jour d'une variable globale oubliée)
  → Rendre les effets de bord explicites avec les contrats Global/Depends (section 9)

5. Prouver l’absence de dépassement ── Garantir la sécurité numérique

L’une des choses les plus précieuses en pratique que SPARK peut prouver est l’absence de dépassement (overflow).

Considérez ce code :

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

Pre => X < Integer'Last est la clé. Avec ce contrat, GNATprove peut prouver que l’addition ne débordera pas.

Sans contrat, GNATprove avertit d’un dépassement possible :

medium: overflow check might fail

Il en va de même pour des calculs plus complexes :

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 semble complexe, mais elle exprime simplement que « la somme A+B ne déborde pas », en distinguant les cas selon le signe.

Point clé :
  L'essence de la preuve d'absence de dépassement consiste à déclarer,
  dans Pre, que le résultat d'une addition ou d'une multiplication tient
  dans les bornes du type
  Cela peut sembler fastidieux, mais une fois écrit, plus jamais de bogue
  de dépassement ne viendra vous tourmenter

6. Invariants de boucle ── Prouver les propriétés des boucles

L’une des parties les plus difficiles de la vérification formelle est la preuve des boucles.

Les boucles s’exécutent un nombre arbitraire de fois, si bien que les tests ne peuvent pas couvrir tous les cas. SPARK utilise pour cela les invariants de boucle (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;

Concevoir des invariants de boucle exige la démarche suivante :

1. Écrire une propriété vraie au début de chaque itération
2. En choisir une qui, après la dernière itération, implique la Post recherchée
3. L'invariant exprime le calcul partiel effectué jusqu'à ce point sous forme de formule

Voici un autre exemple : la recherche dans un tableau.

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;

L’invariant ici est : « dans la plage examinée jusqu’ici, Target n’existe pas ».

Principes de conception des invariants de boucle :
  Exprimer sous forme de formule : « après n itérations, que peut-on affirmer ? »
  Pour les boucles sur tableau, le motif habituel est « pour la plage déjà traitée, P est vraie »
  Un invariant trop fort ne peut pas être prouvé ; trop faible, il n'implique pas la Post
  Trouver le bon équilibre est tout l'art de la preuve de boucles

7. Pragmas d’assertion ── Propriétés partielles dans le code

En plus des contrats (Pre/Post), SPARK permet d’écrire des assertions (Assert) au cœur même du code.

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;

Usage des différents pragmas :

Pre/Post :       Promesses à l'entrée et à la sortie du sous-programme
Assert :         Une propriété qui doit être vraie à un point précis du code
Loop_Invariant : Une propriété préservée à chaque itération de boucle
Loop_Variant :   Une quantité décroissante prouvant la terminaison de la boucle

Bons cas d’usage pour Assert :

Vérifier les résultats intermédiaires de calculs complexes
Vérifier l'état après une branche if/else
Confirmer des propriétés des valeurs de retour après un appel de procédure
Fournir des lemmes qui facilitent les preuves suivantes

8. Contrats de flux de données ── Global et Depends

L’une des fonctionnalités puissantes de SPARK est celle des contrats de flux de données.

Ils déclarent explicitement quelles variables globales un sous-programme lit et écrit.

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;

Les modes du contrat Global sont les suivants :

Input :  lecture seule (pour les fonctions)
Output : écriture seule (pour l'initialisation)
In_Out : lecture et écriture (pour les mises à jour)

De plus, les dépendances entre variables peuvent être exprimées avec Depends :

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

=>+ signifie « dépend de la valeur précédente, plus ces entrées supplémentaires ».

Avantages des contrats de flux de données :
  1. « Que touche cette fonction ? » se voit d'un coup d'œil
  2. Les effets de bord non désirés sont détectés à la compilation
  3. Ils alimentent l'analyse de flux d'information des variables
  4. Ils aident à visualiser le flux de données dans les grands systèmes

9. Niveaux de preuve ── Adoption progressive de Stone à Platinum

SPARK définit le concept de niveaux de preuve (Proof Levels).

Tenter de prouver tout le code d’un seul coup mène souvent au découragement. SPARK propose donc une stratégie d’augmentation progressive de la rigueur des preuves.

Stone (niveau 0) :
  Vérification de la syntaxe des contrats et de la cohérence des types uniquement
  Le premier niveau à atteindre

Bronze (niveau 1) :
  Stone + preuve de l'absence de lecture de variables non initialisées
  Garantie de correction de base

Silver (niveau 2) :
  Bronze + preuve de l'absence d'erreurs d'exécution (dépassement de
  bornes, overflow, division par zéro)
  L'objectif le plus pragmatique

Gold (niveau 3) :
  Silver + preuve des conditions Pre/Post
  Garantie de correction fonctionnelle complète

Platinum (niveau 4) :
  Gold + preuve de la non-interférence des données et du flux d'information
  Pour les systèmes où la sécurité prime

Une stratégie d’adoption pratique :

Phase 1 : amener l'ensemble du projet au niveau Stone
  → Repérer les erreurs d'écriture des contrats

Phase 2 : amener les modules critiques au niveau Silver
  → Éliminer les dépassements et les accès hors bornes
  → La plupart des bogues réels sont évités à ce stade

Phase 3 : prouver la logique centrale au niveau Gold
  → Garantir mathématiquement la correction fonctionnelle
  → Prouver la correction des algorithmes

Phase 4 : passer à Platinum si des exigences de sécurité l'imposent
  → Détecter les chemins de fuite d'information

10. Un flux de preuve pratique ── Réduire les retours en arrière

Voici un flux de travail pour utiliser GNATprove au quotidien :

1. Concevoir les types et les spécifications
   Décider des contraintes de plage et des invariants de type

2. Écrire les contrats (Pre/Post)
   Exprimer la spécification sous forme de contrats avant l'implémentation

3. Faire compiler le code
   Corriger les erreurs de compilation avec GNAT

4. Exécuter GNATprove au niveau Stone
   gnatprove -P proj.gpr --level=0

5. Examiner les avertissements et affiner les contrats si nécessaire
   Porter une attention particulière aux problèmes d'initialisation

6. Viser le niveau Silver
   gnatprove -P proj.gpr --level=2
   Éliminer toutes les erreurs d'exécution

7. Ajouter des invariants de boucle si nécessaire
   Si une preuve échoue, vérifier si des invariants manquent

8. Prouver la correction fonctionnelle au niveau Gold
   gnatprove -P proj.gpr --level=3

Situations « impossible à prouver » fréquentes et leur traitement :

Cas 1 : « medium: postcondition might fail »
  → Post trop forte, ou Pre trop faible
  → Ou invariants de boucle insuffisants

Cas 2 : « medium: overflow check might fail »
  → Restreindre les plages de valeurs dans Pre
  → Ou réduire la plage du type lui-même

Cas 3 : « medium: array index check might fail »
  → Utiliser un invariant de boucle pour montrer que la plage de la boucle
    reste dans les bornes du tableau
  → Utiliser for I in Arr'Range pour aider la reconnaissance automatique
    des bornes par SPARK

Cas 4 : « prover timeout »
  → Le solveur a expiré ; découper la preuve en invariants progressifs
  → Diviser les grandes fonctions en fonctions plus petites

11. Combiner SPARK et les tests ── Comprendre la relation de complémentarité

La vérification formelle et les tests ne s’opposent pas ; ils se complètent.

Preuves SPARK :
  Prouvent des propriétés pour toutes les entrées possibles
  Ne couvrent que les propriétés écrites dans les contrats
  Les cas non prouvables sont confiés à la revue manuelle ou aux tests

Tests :
  Vérifient le comportement réel pour les entrées sélectionnées
  Peuvent révéler des hypothèses implicites non écrites dans les contrats
  Peuvent vérifier l'interaction avec l'environnement d'exécution

Motifs d’utilisation combinée :

1. Garantir l'absence d'erreurs d'exécution (niveau Silver) avec SPARK
2. Vérifier la correction concrète des entrées/sorties avec des tests unitaires
3. Prouver la logique centrale au niveau Gold
4. Concentrer les tests sur les parties non prouvables

Ada dispose du framework de tests unitaires AUnit. Une combinaison pratique consiste à solidifier les types et les contrats avec SPARK, puis à tester le comportement avec AUnit.

12. Lire les résultats de GNATprove ── Interpréter les messages

La sortie de GNATprove comporte trois niveaux de sévérité :

info :   preuve réussie
medium : preuve échouée (avertissement). Revue manuelle nécessaire
high :   preuve échouée (erreur). Violation de contrat probable

Messages fréquents et leur signification :

« postcondition proved »          la condition Post a été prouvée
« range check proved »            la vérification de plage a été prouvée
« overflow check proved »         l'absence de dépassement a été prouvée
« index check proved »            les bornes d'indice de tableau ont été prouvées
« divide by zero check proved »   l'absence de division par zéro a été prouvée

« might fail »                    n'a pas pu être prouvé
« cannot prove »                  le solveur n'a pas pu achever la preuve
« prover timeout »                la preuve n'a pas abouti dans le délai imparti

Procédure à suivre face à might fail :

1. Lire le code et juger s'il peut réellement échouer
2. Si oui, corriger le code
3. S'il ne devrait pas échouer, renforcer le contrat (Pre / invariant)
4. Si la preuve reste impossible, déclarer une hypothèse avec pragma Assume
   (attention : Assume est une hypothèse non prouvée, à utiliser avec prudence)

13. Intégration dans des projets réels

Voici une approche réaliste pour introduire SPARK dans un projet existant :

1. Commencer par le nouveau code
   Ne pas tenter de convertir tout le code existant en SPARK d'un seul coup
   Activer SPARK_Mode sur les modules nouvellement écrits

2. Viser Silver
   Gold (preuve fonctionnelle complète) est idéal, mais on commence par
   Silver (absence d'erreurs d'exécution)
   La seule prévention des dépassements apporte déjà une valeur pratique
   considérable

3. Écrire les contrats en partant des interfaces
   Écrire les contrats dans la spécification du package (.ads) avant l'implémentation
   Avec une spécification solide, n'importe quel développeur peut écrire
   un code qui satisfait les contrats

4. Intégrer dans le CI/CD
   Ajouter gnatprove au pipeline d'intégration continue
   Arrêter le build (ou au moins avertir) en cas d'échec de preuve

5. Accumuler des rapports de preuve
   Générer des rapports avec gnatprove --report=all
   Suivre l'évolution des éléments non prouvés dans le temps

Pour les projets mêlant code C/C++ et Ada, une approche progressive est efficace :

1. Écrire les nouveaux modules en Ada/SPARK
2. Communiquer avec C/C++ via Interfaces.C
3. Migrer les structures de données critiques et la logique de vérification vers SPARK
4. Étendre progressivement la couverture SPARK

14. Limites et précautions concernant SPARK

SPARK n’est pas non plus une solution miracle. Comprendre honnêtement ses limites permet une application correcte.

Ce que SPARK peut prouver :
  SPARK ne prouve que les propriétés écrites dans les contrats
  Les propriétés omises (oubliées à l'écriture) ne sont pas prouvées
  Exemple : prouver dans Post que le résultat est trié ne garantit pas
  que les éléments d'origine sont préservés, à moins de l'écrire aussi

Limites des solveurs :
  Certaines propriétés complexes dépassent les capacités des solveurs
  automatiques
  Dans ce cas, une preuve interactive (Coq, etc.) est nécessaire
  Cela dit, la preuve automatique suffit dans la plupart des cas pratiques

Restrictions du langage :
  Le code fortement basé sur des pointeurs ne peut pas être converti en SPARK
  La preuve de l'allocation dynamique de mémoire est limitée
  La preuve des structures de données récursives est difficile

Maîtrise des développeurs :
  Écrire des contrats demande de l'entraînement
  Concevoir des invariants de boucle est particulièrement long à maîtriser
  Un plan de montée en compétence pour toute l'équipe est indispensable

15. Conclusion ── Faire de la preuve un geste quotidien du développement

Nous avons parcouru la pratique de la vérification formelle avec SPARK.

SPARK est un sous-ensemble d'Ada, restreint aux fonctionnalités vérifiables
Les contrats (Pre/Post) sont l'entrée des preuves. Les contrats d'Ada 2012
fonctionnent directement
GNATprove exécute des preuves automatiques et rapporte les résultats au
niveau du code source
Les invariants de boucle prouvent les propriétés des boucles
Global/Depends rendent le flux de données explicite et gèrent les effets
de bord
Les niveaux de preuve (de Stone à Platinum) permettent d'augmenter la
rigueur par étapes
Viser d'abord le niveau Silver (absence d'erreurs d'exécution) est la
recommandation pratique
Tests et preuves ne s'opposent pas — ils se complètent

On pourrait avoir l’idée reçue que « la vérification formelle est trop difficile et réservée à des projets particuliers ».

Mais la combinaison actuelle de SPARK et GNATprove a atteint le niveau suivant :

1. Écrire un contrat. C'est fondamentalement la même démarche de
   conception que d'écrire des types ou des tests
2. Exécuter gnatprove. Cela ressemble à une compilation
3. Regarder les résultats et corriger le code ou le contrat

Ce cycle ne diffère en rien du flux de développement quotidien où l’on corrige du code en lisant les messages d’erreur du compilateur.

La différence est la suivante : là où un compilateur garantit que « la syntaxe est correcte », GNATprove garantit « la correction pour toutes les entrées ».

La devise d’Ada présentée dans l’article précédent — « les bogues ne sont pas des choses qu’on trouve ; les types et les contrats les rendent impossibles à écrire » — franchit une étape supplémentaire avec SPARK :

L’absence de bogue est garantie par la preuve.

Commencez par ajouter SPARK_Mode et un Post à une petite fonction, puis exécutez gnatprove.

En voyant apparaître le message vert postcondition proved, votre regard sur l’assurance qualité logicielle changera.

Références

Articles associés

Articles récents partageant les mêmes étiquettes, pour approfondir des sujets proches.

Sujets associés

Ces pages replacent le sujet dans un contexte plus large de services et de décisions.

Questions fréquentes

Questions souvent posées lors d’une consultation sur le sujet de cet article.

Qu'est-ce que SPARK et quel est son rapport avec Ada ?
SPARK est un sous-ensemble délibérément restreint d'Ada, conçu pour que les propriétés d'un programme puissent être prouvées mathématiquement. Il limite les fonctionnalités difficiles à vérifier — usage libre des pointeurs, gestion illimitée des exceptions, structures de données récursives et tâches sans restriction — en échange de la prouvabilité. Le code SPARK est du code Ada auquel s'ajoutent des annotations de contrat : il s'agit donc d'un prolongement naturel du développement Ada courant, et non d'un langage différent. L'outil GNATprove traduit les contrats vers le langage intermédiaire Why3 et tente des preuves avec des solveurs automatiques comme Z3, CVC4 et Alt-Ergo.
En quoi la vérification formelle avec SPARK diffère-t-elle des tests ?
Les tests vérifient que le programme se comporte correctement pour les entrées choisies ; la vérification formelle prouve mathématiquement qu'une propriété est vraie pour toutes les entrées possibles. Les deux approches se complètent plutôt qu'elles ne s'opposent : SPARK ne prouve que les propriétés écrites dans les contrats, tandis que les tests peuvent révéler des hypothèses implicites jamais formalisées et vérifier l'interaction avec l'environnement d'exécution. Une combinaison pratique consiste à garantir l'absence d'erreurs d'exécution avec SPARK, à vérifier des comportements d'entrée/sortie concrets avec des tests unitaires, et à concentrer les tests sur les parties qui ne peuvent pas être prouvées.
Quels sont les niveaux de preuve de SPARK, et lequel viser en premier ?
SPARK définit cinq niveaux de rigueur croissante : Stone (syntaxe des contrats et cohérence des types), Bronze (ajoute la preuve d'absence de lectures non initialisées), Silver (ajoute la preuve d'absence d'erreurs d'exécution telles que dépassements, violations de bornes et division par zéro), Gold (ajoute la preuve de correction fonctionnelle des conditions Pre/Post) et Platinum (ajoute la non-interférence des données et le flux d'information). Silver est l'objectif initial le plus pragmatique — la plupart des bogues réels sont éliminés en supprimant les erreurs d'exécution — et Gold vaut la peine d'être visé pour la logique centrale dont la correction doit être garantie.
Qu'est-ce qu'un invariant de boucle, et pourquoi les preuves SPARK en ont-elles besoin ?
Un invariant de boucle est une propriété vraie au début de chaque itération, exprimée avec pragma Loop_Invariant. Les boucles s'exécutent un nombre arbitraire de fois, si bien que le prouveur a besoin de l'invariant pour raisonner sur toutes les itérations à la fois : il exprime le calcul partiel accompli jusque-là sous forme de formule, et après la dernière itération il doit impliquer la postcondition recherchée. Concevoir des invariants est la compétence la plus délicate dans les preuves de boucle : un invariant trop fort ne peut pas être prouvé, tandis qu'un invariant trop faible n'implique pas la postcondition.

Profil de l’auteur

Page de présentation de l’auteur de l’article.

Go Komura

Représentant de KomuraSoft LLC

Spécialisé dans le développement de logiciels Windows, le conseil technique et l’analyse de pannes, notamment pour les systèmes existants et les incidents difficiles à reproduire.

Nous contacter
Retour au blog