Licence CC BY-NC-SA

Instructions basiques et structures de contrôle

Dernière mise à jour :

Cette partie est plus formelle que ce nous avons vu jusqu’à maintenant. Si le lecteur souhaite se concentrer sur l’utilisation de l’outil, l’introduction de ce chapitre et les deux premières sections (sur les instructions de base et « le bonus stage ») sont dispensables. Si ce que nous avons présenté jusqu’à maintenant a semblé ardu au lecteur sur un plan formel, il est également possible de réserver l’introduction et ces deux sections pour une deuxième lecture.

Les sections sur les boucles sont en revanches indispensables. Les éléments plus formels de ces sections seront signalés.

Pour chaque notion en programmation C, nous associerons la règle d’inférence qui lui correspond, la règle utilisée de calcul de plus faible pré-conditions qui la régit, et des exemples d’utilisation. Pas forcément dans cet ordre et avec plus ou moins de liaison avec l’outil. Les premiers points seront plus focalisés sur la théorie que sur l’utilisation car ce sont les plus simples, au fur et à mesure, nous nous concentrerons de plus en plus sur l’outil, en particulier quand nous attaquerons le point concernant les boucles.

Règle d’inférence

Une règle d’inférence est de la forme :

$\dfrac{P_1 \quad ... \quad P_n}{C}$

Et signifie que pour assurer que la conclusion $C$ est vraie, il faut d’abord savoir que les prémisses $P_1$, …, et $P_n$ sont vraies. Quand il n’y a pas de prémisses :

$\dfrac{}{\quad C \quad}$

Alors, il n’y a rien à assurer pour conclure que $C$ est vraie.

Inversement, pour prouver qu’une certaine prémisse est vraie, il peut être nécessaire d’utiliser une autre règle d’inférence, ce qui nous donnerait quelque chose comme :

$\dfrac{\dfrac{}{\quad P_1\quad} \quad \dfrac{P_{n_1}\quad P_{n_2}}{P_n}}{C}$

Ce qui nous construit progressivement l’arbre de déduction de notre raisonnement. Dans notre raisonnement, les prémisses et conclusions manipulées seront généralement des triplets de Hoare.

Triplet de Hoare

Revenons sur la notion de triplet de Hoare :

$\{ P \}\quad C\quad \{ Q \}$

Nous l’avons vu en début de tutoriel, ce triplet nous exprime que si avant l’exécution de $C$, la propriété $P$ est vraie, et si $C$ termine, alors la propriété $Q$ est vraie. Par exemple, si nous reprenons notre programme de calcul de la valeur absolue (légèrement modifié):

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
/*@
  ensures \result >= 0;
  ensures (val >= 0 ==> \result == val ) && (val <  0 ==> \result == -val);
*/
int abs(int val){
  int res;
  if(val < 0) res = - val;
  else        res = val;

  return res;
}

Ce que nous dit Hoare, est que pour prouver notre programme, les propriétés entre accolades dans ce programme doivent être vérifiées (j’ai omis une des deux post-conditions pour alléger la lecture) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
int abs(int val){
  int res;
// { P }
  if(val < 0){
// {  (val < 0) && P }
    res = - val;
// { \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val }
  } else {
// { !(val < 0) && P }
    res = val;
// { \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val }
  }
// { \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val }

  return res;
}

Cependant, Hoare ne nous dit pas comment nous pouvons obtenir automatiquement la propriété P de ce programme. Ce que nous propose Dijkstra, c’est donc un moyen de calculer, à partir d’une post-condition $Q$ et d’une commande ou d’une liste de commandes $C$, la pré-condition minimale assurant $Q$ après $C$. Nous pourrions donc, dans le programme précédent, calculer la propriété P qui nous donne les garanties voulues.

Nous allons tout au long de cette partie présenter les différents cas de la fonction $wp$ qui, à une post-condition voulue et un programme ou une instruction, nous associe la plus faible pré-condition qui permet de l’assurer. Nous utiliserons cette notation pour définir le calcul correspondant à une/des instructions :

$wp(Instruction(s), Post) := WeakestPrecondition$

Et la fonction $wp$ est telle qu’elle nous garantit que le triplet de Hoare :

$\{\ wp(C,Q)\ \}\quad C\quad \{ Q \}$

est effectivement un triplet valide.

Nous utiliserons souvent des assertions ACSL pour présenter les notions à venir :

1
//@ assert ma_propriete ;

Ces assertions correspondent en fait à des étapes intermédiaires possibles pour les propriétés indiquées dans nos triplets de Hoare. Nous pouvons par exemple reprendre le programme précédent et remplacer nos commentaires par les assertions ACSL correspondantes (j’ai omis P car sa valeur est en fait simplement « vrai ») :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
int abs(int val){
  int res;
  if(val < 0){
    //@ assert val < 0 ;
    res = - val;
    //@ assert \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val ;
  } else {
    //@ assert !(val < 0) ;
    res = val;
    //@ assert \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val ;
  }
  //@ assert \at(val, Pre) >= 0 ==> res == val && \at(val, Pre) < 0 ==> res == -val ;

  return res;
}

Affectation, séquence et conditionnelle

Affectation

L’affectation est l’opération la plus basique que l’on puisse avoir dans un langage (mise à part l’opération « ne rien faire » qui manque singulièrement d’intérêt). Le calcul de plus faible pré-condition associé est le suivant :

$wp(x = E , Post) := Post[x \leftarrow E]$

Où la notation $P[x \leftarrow E]$ signifie « la propriété $P$$x$ est remplacé par $E$ ». Ce qui correspond ici à « la post-condition $Post$$x$ a été remplacé par $E$ ». Dans l’idée, pour que la formule en post-condition d’une affectation de $x$ à $E$ soit vraie, il faut qu’elle soit vraie en remplaçant chaque occurrence de $x$ dans la formule par $E$. Par exemple :

1
2
3
// { P }
x = 43 * c ;
// { x = 258 }

$P = wp(x = 43*c , \{x = 258\}) = \{43*c = 258\}$

La fonction $wp$ nous permet donc de calculer la plus faible pré-condition de l’opération ($\{43*c = 258\}$), ce que l’on peut réécrire sous la forme d’un triplet de Hoare :

1
2
3
// { 43*c = 258 }
x = 43 * c ;
// { x = 258 }

Pour calculer la pré-condition de l’affectation, nous avons remplacé chaque occurrence de $x$ dans la post-condition, par la valeur $E = 43*c$ affectée. Si notre programme était de la forme:

1
2
3
4
int c = 6 ;
// { 43*c = 258 }
x = 43 * c ;
// { x = 258 }

Nous pourrions alors fournir la formule « $43*6 = 258$ » à notre prouveur automatique afin qu’il détermine si cette formule peut effectivement être satisfaite. Ce à quoi il répondrait évidemment « oui » puisque cette propriété est très simple à vérifier. En revanche, si nous avions donné la valeur 7 pour c, le prouveur nous répondrait que non, une telle formule n’est pas vraie.

Nous pouvons donc écrire la règle d’inférence pour le triplet de Hoare de l’affectation, où l’on prend en compte le calcul de plus faible pré-condition :

$\dfrac{}{\{Q[x \leftarrow E] \}\quad x = E \quad\{ Q \}}$

Nous noterons qu’il n’y a pas de prémisse à vérifier. Cela veut-il dire que le triplet est nécessairement vrai ? Oui. Mais cela ne dit pas si la pré-condition est respectée par le programme où se trouve l’instruction, ni que cette pré-condition est possible. C’est ce travail qu’effectuent ensuite les prouveurs automatiques.

Par exemple, nous pouvons demander la vérification de la ligne suivante avec Frama-C :

1
2
int a = 42;
//@ assert a == 42;

Ce qui est, bien entendu, prouvé directement par Qed car c’est une simple application de la règle de l’affectation.

Notons que d’après la norme C, l’opération d’affectation est une expression et non une instruction. C’est ce qui nous permet par exemple d’écrire if( (a = foo()) == 42). Dans Frama-C, une affectation sera toujous une instruction. En effet, si une affectation est présente au sein d’une expression plus complexe, le module de création de l’arbre de syntaxe abstraite du programme analysé effectue une étape de normalisation qui crée systématiquement une instruction séparée.

Séquence d’instructions

Pour qu’une instruction soit valide, il faut que sa pré-condition nous permette, par cette instruction, de passer à la post-condition voulue. Maintenant, nous avons besoin d’enchaîner ce processus d’une instruction à une autre. L’idée est alors que la post-condition assurée par la première instruction soit compatible avec la pré-condition demandée par la deuxième et que ce processus puisse se répéter pour la troisième instruction, etc.

La règle d’inférence correspondant à cette idée, utilisant les triplets de Hoare est la suivante:

$\dfrac{\{P\}\quad S1 \quad \{R\} \ \ \ \{R\}\quad S2 \quad \{Q\}}{\{P\}\quad S1 ;\ S2 \quad \{Q\}}$

Pour vérifier que la séquence d’instructions $S1;\ S2$ (NB : où $S1$ et $S2$ peuvent elles-mêmes être des séquences d’instructions), nous passons par une propriété intermédiaire qui est à la fois la pré-condition de $S2$ et la post-condition de $S1$. Cependant, rien ne nous indique pour l’instant comment obtenir les propriétés $P$ et $R$.

Le calcul de plus faible pré-condition $wp$ nous dit simplement que la propriété intermédiaire $R$ est trouvée par calcul de plus faible pré-condition de la deuxième instruction. Et que la propriété $P$ est trouvée en calculant la plus faible pré-condition de la première instruction. La plus faible pré-condition de notre liste d’instruction est donc déterminée comme ceci :

$wp(S1;\ S2 , Post) := wp(S1, wp(S2, Post) )$

Le plugin WP de Frama-C fait ce calcul pour nous, c’est pour cela que nous n’avons pas besoin d’écrire les assertions entre chaque ligne de code.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
int main(){
  int a = 42;
  int b = 37;

  int c = a+b; // i:1
  a -= c;      // i:2
  b += a;      // i:3

  //@assert b == 0 && c == 79;
}

Arbre de preuve

Notons que lorsque nous avons plus de deux instructions, nous pouvons simplement considérer que la dernière instruction est la seconde instruction de notre règle et que toutes les instructions qui la précède forment la première « instruction ». De cette manière nous remontons bien les instructions une à une dans notre raisonnement, par exemple avec le programme précédent :

$\{P\}\quad i_1 ; \quad \{Q_{-2}\}$

$\{Q_{-2}\}\quad i_2 ; \quad \{Q_{-1}\}$

$\{P\}\quad i_1 ; \quad i_2 ; \quad \{Q_{-1}\}$

$\{Q_{-1}\} \quad i_3 ; \quad \{Q\}$

$\{P\}\quad i_1 ; \quad i_2 ; \quad i_3 ; \quad \{ Q \}$

Nous pouvons par calcul de plus faibles pré-conditions construire la propriété $Q_{-1}$ à partir de $Q$ et $i_3$, ce qui nous permet de déduire $Q_{-2}$, à partir de $Q_{-1}$ et $i_2$ et finalement $P$ avec $Q_{-2}$ et $i_1$.

Nous pouvons maintenant vérifier des programmes comprenant plusieurs instructions, il est temps d’y ajouter un peu de structure.

Règle de la conditionnelle

Pour qu’un branchement conditionnel soit valide, il faut que la post-condition soit atteignable par les deux banches, depuis la même pré-condition, à ceci près que chacune des branches aura une information supplémentaire : le fait que la condition était vraie dans un cas et fausse dans l’autre.

Comme avec la séquence d’instructions, nous aurons donc deux points à vérifier (pour éviter de confondre les accolades, j’utilise la syntaxe $if\ B\ then\ S1\ else\ S2$) :

$\dfrac{\{P \wedge B\}\quad S1\quad \{Q\} \quad \quad \{P \wedge \neg B\}\quad S2\quad \{Q\}}{\{P\}\quad if\quad B\quad then\quad S1\quad else\quad S2 \quad \{Q\}}$

Nos deux prémisses sont donc la vérification que lorsque nous avons la pré-condition et que nous passons dans la branche if, nous atteignons bien la post-condition, et que lorsque nous avons la pré-condition et que nous passons dans la branche else, nous obtenons bien également la post-condition.

Le calcul de pré-condition de $wp$ pour la conditionnelle est le suivant :

$wp(if\ B\ then\ S1\ else\ S2 , Post) := (B \Rightarrow wp(S1, Post)) \wedge (\neg B \Rightarrow wp(S2, Post))$

À savoir que $B$ doit impliquer la pré-condition la plus faible de $S1$, pour pouvoir l’exécuter sans erreur vers la post-condition, et que $\neg B$ doit impliquer la pré-condition la plus faible de $S2$ (pour la même raison).

Bloc else vide

En suivant cette définition, si le else ne fait rien, alors la règle d’inférence est de la forme suivante, en remplaçant $S2$ par une instruction « ne rien faire ».

$\dfrac{\{P \wedge B\}\quad S1\quad \{Q\} \quad \quad \{P \wedge \neg B\}\quad skip\quad \{Q\}}{\{P\}\quad if\quad B\quad then\quad S1\quad else\quad skip \quad \{Q\}}$

Le triplet pour le else est :

$\{P \wedge \neg B\}\quad skip\quad \{Q\}$

Ce qui veut dire que nous devons avoir :

$P \wedge \neg B \Rightarrow Q$

En résumé, si la condition du if est fausse, cela veut dire que la post-condition de l’instruction conditionnelle globale est déjà vérifiée avant de rentrer dans le else (puisqu’il ne fait rien).

Par exemple, nous pourrions vouloir remettre une configuration $c$ à une valeur par défaut si elle a mal été configurée par un utilisateur du programme :

1
2
3
4
5
6
7
8
int c;

// ... du code ...

if(c < 0 || c > 15){
  c = 0;
}
//@ assert 0 <= c <= 15;

Soit :

$wp(if \neg (c \in [0;15])\ then\ c := 0, \{c \in [0;15]\})$

$:= (\neg (c \in [0;15])\Rightarrow wp(c := 0, \{c \in [0;15]\})) \wedge (c \in [0;15]\Rightarrow wp(skip, \{c \in [0;15]\}))$

$= (\neg (c \in [0;15]) \Rightarrow 0 \in [0;15]) \wedge (c \in [0;15] \Rightarrow c \in [0;15])$

$= (\neg (c \in [0;15]) \Rightarrow true) \wedge true$

La formule est bien vérifiable : quelle que soit l’évaluation de $\neg (c \in [0;15])$ l’implication sera vraie.

[Bonus Stage] Conséquence et constance

Règle de conséquence

Parfois, il peut être utile pour la preuve de renforcer une post-condition ou d’affaiblir une pré-condition. Si la première sera souvent établie par nos soins pour faciliter le travail du prouveur, la seconde est plus souvent vérifiée par l’outil à l’issu du calcul de plus faible pré-condition.

La règle d’inférence en logique de Hoare est la suivante :

$\dfrac{P \Rightarrow WP \quad \{WP\}\quad c\quad \{SQ\} \quad SQ \Rightarrow Q}{\{P\}\quad c \quad \{Q\}}$

(Nous noterons que les prémisses, ici, ne sont pas seulement des triplets de Hoare mais également des formules à vérifier)

Par exemple, si notre post-condition est trop complexe, elle risque de générer une plus faible pré-condition trop compliquée et de rendre le calcul des prouveurs difficile. Nous pouvons alors créer une post-condition intermédiaire $SQ$, plus simple, mais plus restreinte et impliquant la vraie post-condition. C’est la partie $SQ \Rightarrow Q$.

Inversement, le calcul de pré-condition générera généralement une formule compliquée et souvent plus faible que la pré-condition que nous souhaitons accepter en entrée. Dans ce cas, c’est notre outil qui s’occupera de vérifier l’implication entre ce que nous voulons et ce qui est nécessaire pour que notre code soit valide. C’est la partie $P \Rightarrow WP$.

Nous pouvons par exemple illustrer cela avec le code qui suit. Notons bien qu’ici, le code pourrait tout à fait être prouvé par l’intermédiaire de WP sans ajouter des affaiblissements et renforcements de propriétés car le code est très simple, il s’agit juste d’illustrer la règle de conséquences.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
/*@
  requires P: 2 <= a <= 8;
  ensures  Q: 0 <= \result <= 100 ;
  assigns  \nothing ;
*/
int constrained_times_10(int a){
  //@ assert P_imply_WP: 2 <= a <= 8 ==> 1 <= a <= 9 ;
  //@ assert WP:         1 <= a <= 9 ;

  int res = a * 10;

  //@ assert SQ:         10 <= res <= 90 ;
  //@ assert SQ_imply_Q: 10 <= res <= 90 ==> 0 <= res <= 100 ;

  return res;
}

(À noter ici : nous avons omis les contrôles de débordement d’entiers).

Ici, nous voulons avoir un résultat compris entre 0 et 100. Mais nous savons que le code ne produira pas un résultat sortant des bornes 10 à 90. Donc nous renforçons la post-condition avec une assertion que res, le résultat, est compris entre 0 et 90 à la fin. Le calcul de plus faible pré-condition, sur cette propriété, et avec l’affectation res = 10*a nous produit une plus faible pré-condition 1 <= a <= 9 et nous savons finalement que 2 <= a <= 8 nous donne cette garantie.

Quand une preuve a du mal à être réalisée sur un code plus complexe, écrire des assertions produisant des post-conditions plus fortes mais qui forment des formules plus simples peut souvent nous aider. Notons que dans le code précédent, les lignes P_imply_WP et SQ_imply_Q ne sont jamais utiles car c’est le raisonnement par défaut produit par WP, elles sont juste présentes pour l’illustration.

Règle de constance

Certaines séquences d’instructions peuvent concerner et faire intervenir des variables différentes. Ainsi, il peut arriver que nous initialisions et manipulions un certain nombre de variables, que nous commencions à utiliser certaines d’entre elles, puis que nous les délaissions au profit d’autres pendant un temps. Quand un tel cas apparaît, nous avons envie que l’outil ne se préoccupe que des variables qui sont susceptibles d’être modifiées pour avoir des propriétés les plus légères possibles.

La règle d’inférence qui définit ce raisonnement est la suivante :

$\dfrac{\{P\}\quad c\quad \{Q\}}{\{P \wedge R\}\quad c\quad \{Q \wedge R\}}$

$c$ ne modifie aucune variable entrant en jeu dans $R$. Ce qui nous dit : « pour vérifier le triplet, débarrassons nous des parties de la formule qui concerne des variables qui ne sont pas manipulées par $c$ et prouvons le nouveau triplet ». Cependant, il faut prendre garde à ne pas supprimer trop d’informations, au risque de ne plus pouvoir prouver nos propriétés.

Par exemple, nous pouvons imaginer le code suivant (une nouvelle fois, nous omettons les contrôles de débordements au niveau des entiers) :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
/*@
  requires a > -99 ;
  requires b > 100 ;
  ensures  \result > 0 ;
  assigns  \nothing ;
*/
int foo(int a, int b){
  if(a >= 0){
    a++ ;
  } else {
    a += b ;
  }
  return a ;
}

Si nous regardons le code du bloc if, il ne fait pas intervenir la variable b, donc nous pouvons omettre complètement les propriétés à propos de b pour réaliser la preuve que a sera bien supérieur à 0 après l’exécution du bloc :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
/*@
  requires a > -99 ;
  requires b > 100 ;
  ensures  \result > 0 ;
  assigns  \nothing ;
*/
int foo(int a, int b){
  if(a >= 0){
    //@ assert a >= 0; //et rien à propos de b
    a++ ;
  } else {
    a += b ;
  }
  return a ;
}

En revanche, dans le bloc else, même si b n’est pas modifiée, établir des propriétés seulement à propos de a rendrait notre preuve impossible (en tant qu’humains). Le code serait :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
/*@
  requires a > -99 ;
  requires b > 100 ;
  ensures  \result > 0 ;
  assigns  \nothing ;
*/
int foo(int a, int b){
  if(a >= 0){
    //@ assert a >= 0; // et rien à propos de b
    a++ ;
  } else {
    //@ assert a < 0 && a > -99 ; // et rien à propos de b
    a += b ;
  }
  return a ;
}

Dans le bloc else, n’ayant que connaissance du fait que a est compris entre -99 et 0, et ne sachant rien à propos de b, nous pourrions difficilement savoir si le calcul a += b produit une valeur supérieure strict à 0 pour a.

Naturellement ici, WP prouvera la fonction sans problème, puisqu’il transporte de lui-même les propriétés qui lui sont nécessaires pour la preuve. En fait, l’analyse des variables qui sont nécessaires ou non (et l’application, par conséquent de la règle de constance) est réalisée directement par WP.

Notons finalement que la règle de constance est une instance de la règle de conséquence :

$\dfrac{P \wedge R \Rightarrow P \quad \{P\}\quad c\quad \{Q\} \quad Q \Rightarrow Q \wedge R}{\{P \wedge R\}\quad c\quad \{Q \wedge R\}}$

Si les variables de $R$ n’ont pas été modifiées par l’opération (qui par contre, modifie les variables de $P$ pour former $Q$), alors effectivement $P \wedge R \Rightarrow P$ et $Q \Rightarrow Q \wedge R$.

Les boucles

Les boucles ont besoin d’un traitement de faveur dans la vérification déductive de programmes. Ce sont les seules structures de contrôle qui vont nécessiter un travail conséquent de notre part. Nous ne pouvons pas y échapper car sans les boucles nous pouvons difficilement prouver des programmes intéressants.

Avant de s’intéresser à la spécification des boucles, il est légitime de se poser la question suivante : pourquoi les boucles sont-elles compliquées ?

Induction et invariance

La nature des boucles rend leur analyse difficile. Lorsque nous faisons nos raisonnements arrières, il nous faut une règle capable de dire à partir de la post-condition quelle est la pré-condition d’une certaine séquence d’instructions. Problème : nous ne pouvons a priori pas déduire combien de fois la boucle va s’exécuter et donc par conséquent, nous ne pouvons pas non plus savoir combien de fois les variables ont été modifiées.

Nous allons donc procéder en raisonnant par induction. Nous devons trouver une propriété qui est vraie avant de commencer la boucle et qui, si elle est vraie au début d’un tour de boucle, sera vraie à la fin (et donc par extension, au début du tour suivant).

Ce type de propriété est appelé un invariant de boucle. Un invariant de boucle est une propriété qui doit être vraie avant et après chaque tour d’une boucle. Par exemple, pour la boucle :

1
for(int i = 0 ; i < 10 ; ++i){ /* */ }

La propriété $0 <= i <= 10$ est un invariant de la boucle. La propriété $-42 <= i <= 42$ est également un invariant de la boucle (qui est nettement plus imprécis néanmoins). La propriété $0 < i <= 10$ n’est pas un invariant, elle n’est pas vraie à l’entrée de la boucle. La propriété $0 <= i < 10$ n’est pas un invariant de la boucle, elle n’est pas vraie à la fin du dernier tour de la boucle qui met la valeur $i$ à $10$.

Le raisonnement produit par l’outil pour vérifier un invariant $I$ sera donc :

  • vérifions que $I$ est vrai au début de la boucle (établissement),
  • vérifions que $I$ est vrai avant de commencer un tour, auquel cas $I$ est vrai après (préservation).

[Formel] Règle d’inférence

En notant l’invariant $I$, la règle d’inférence correspondant à la boucle est définie comme suit :

$\dfrac{\{I \wedge B \}\ c\ \{I\}}{\{I\}\ while(B)\{c\}\ \{I \wedge \neg B\}}$

Et le calcul de plus faible pré-condition est le suivant :

$wp(while (B) \{ c \}, Post) := I \wedge ((B \wedge I) \Rightarrow wp(c, I)) \wedge ((\neg B \wedge I) \Rightarrow Post)$

Détaillons cette formule :

  • (1) le premier $I$ correspond à l’établissement de l’invariant, c’est vulgairement la « pré-condition » de la boucle,
  • la deuxième partie de la conjonction ($(B \wedge I) \Rightarrow wp(c, I)$) correspond à la vérification du travail effectué par le corps de la boucle :
    • la pré-condition que nous connaissons du corps de la boucle (notons $KWP$, « Known WP ») , c’est ($KWP = B \wedge I$). Soit le fait que nous sommes rentrés dedans ($B$ est vrai), et que l’invariant est respecté à ce moment ($I$, qui est vrai avant de commencer la boucle par 1, et dont veut vérifier qu’il sera vraie en fin de bloc de la boucle (2)),
    • (2) ce qu’il nous reste à vérifier c’est que $KWP$ implique la pré-condition réelle* du bloc de code de la boucle ($KWP \Rightarrow wp(c, Post)$). Ce que nous voulons en fin de bloc, c’est avoir maintenu l’invariant $I$ ($B$ n’est peut-être plus vrai en revanche). Donc $KWP \Rightarrow wp(c, I)$, soit $(B \wedge I) \Rightarrow wp(c, I)$,
    • * cela correspond à une application de la règle de conséquence expliquée précédemment.
  • finalement, la dernière partie ($(\neg B \wedge I) \Rightarrow Post$) nous dit que le fait d’être sorti de la boucle ($\neg B$), tout en ayant maintenu l’invariant $I$, doit impliquer la post-condition voulue pour la boucle.

Dans ce calcul, nous pouvons noter que la fonction $wp$ ne nous donne aucune indication sur le moyen d’obtenir l’invariant $I$. Nous allons donc devoir spécifier manuellement de telles propriétés à propos de nos boucles.

Retour à l’outil

Il existe des outils capables d’inférer des invariants (pour peu qu’ils soient simples, les outils automatiques restent limités). Ce n’est pas le cas de WP. Il nous faut donc écrire nos invariants à la main. Trouver et écrire les invariants des boucles de nos programmes sera toujours la partie la plus difficile de notre travail lorsque nous chercherons à prouver des programmes.

En effet, si en l’absence de boucle, la fonction de calcul de plus faible pré-condition peut nous fournir automatiquement les propriétés vérifiables de nos programmes, ce n’est pas le cas pour les invariants de boucle pour lesquels nous n’avons pas accès à une procédure automatique de calcul. Nous devons donc trouver et formuler correctement ces invariants, et selon l’algorithme, celui-ci peut parfois être très subtil.

Pour indiquer un invariant à une boucle, nous ajoutons les annotations suivantes en début de boucle :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
int main(){
  int i = 0;

  /*@
    loop invariant 0 <= i <= 30;
  */
  while(i < 30){
    ++i;
  }
  //@assert i == 30;
}

RAPPEL : L’invariant est bien : i <= 30 !

Pourquoi ? Parce que tout au long de la boucle i sera bien compris entre 0 et 30 inclus. 30 est même la valeur qui nous permettra de sortir de la boucle. Plus encore, une des propriétés demandées par le calcul de plus faible pré-conditions sur les boucles est que lorsque l’on invalide la condition de la boucle, par la connaissance de l’invariant, on peut prouver la post-condition (Formellement : $(\neg B \wedge I) \Rightarrow Post$).

La post-condition de notre boucle est i == 30 et doit être impliquée par $\neg$ i < 30 $\wedge$ 0 <= i <= 30. Ici, cela fonctionne bien : i >= 30 && 0 <= i <= 30 ==> i == 30. Si l’invariant excluait l’égalité à 30, la post-condition ne serait pas atteignable.

Une nouvelle fois, nous pouvons jeter un œil à la liste des buts dans « WP Goals » :

Obligations générées pour prouver notre boucle

Nous remarquons bien que WP décompose la preuve de l’invariant en deux parties : l’établissement de l’invariant et sa préservation. WP produit exactement le raisonnement décrit plus haut pour la preuve de l’assertion. Dans les versions récentes de Frama-C, Qed est devenu particulièrement puissant, et l’obligation de preuve générée ne le montre pas (affichant simplement « True »). En utilisant l’option -wp-no-simpl au lancement, nous pouvons quand même voir l’obligation correspondante :

Preuve de l’assertion par connaissance de l’invariant et l’invalidation de la condition de boucle

Mais notre spécification est-elle suffisante ?

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
int main(){
  int i = 0;
  int h = 42;

  /*@
    loop invariant 0 <= i <= 30;
  */
  while(i < 30){
    ++i;
  }
  //@assert i == 30;
  //@assert h == 42;
}

Voyons le résultat :

Encore des effets de bord

Il semble que non.

La clause « assigns » … pour les boucles

En fait, à propos des boucles, WP ne considère vraiment que ce que lui fournit l’utilisateur pour faire ses déductions. Et ici l’invariant ne nous dit rien à propos de l’évolution de la valeur de h. Nous pourrions signaler l’invariance de toute variable du programme mais ce serait beaucoup d’efforts. ACSL nous propose plus simplement d’ajouter des annotations assigns pour les boucles. Toute autre variable est considérée invariante. Par exemple :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
int main(){
  int i = 0;
  int h = 42;

  /*@
    loop invariant 0 <= i <= 30;
    loop assigns i;
  */
  while(i < 30){
    ++i;
  }
  //@assert i == 30;
  //@assert h == 42;
}

Cette fois, nous pouvons établir la preuve de correction de la boucle. Par contre, rien ne nous prouve sa terminaison. L’invariant de boucle n’est pas suffisant pour effectuer une telle preuve. Par exemple, dans notre programme, si nous réécrivons la boucle comme ceci :

1
2
3
4
5
6
7
/*@
  loop invariant 0 <= i <= 30;
  loop assigns i;
*/
while(i < 30){

}

L’invariant est bien vérifié également, mais nous ne pourrons jamais prouver que la boucle se termine : elle est infinie.

Correction partielle et correction totale - Variant de boucle

En vérification déductive, il y a deux types de correction, la correction partielle et la correction totale. Dans le premier cas, la formulation est « si la pré-condition est validée et si le calcul termine, alors la post-condition est validée ». Dans le second cas, « si la pré-condition est validée, alors le calcul termine et la post-condition est validée ». WP s’intéresse par défaut à de la preuve de correction partielle :

1
2
3
4
void foo(){
  while(1){}
  //assert \false;
}

Si nous demandons la vérification de ce code en activant le contrôle de RTE, nous obtenons ceci :

Preuve de faux par non-terminaison de boucle

L’assertion « FAUX » est prouvée ! La raison est simple : la non-terminaison de la boucle est triviale : la condition de la boucle est « VRAI » et aucune instruction du bloc de la boucle ne permet d’en sortir puisque le bloc ne contient pas de code du tout. Comme nous sommes en correction partielle, et que le calcul ne termine pas, nous pouvons prouver n’importe quoi au sujet du code qui suit la partie non terminante. Si, en revanche, la non-terminaison est non-triviale, il y a peu de chances que l’assertion soit prouvée.

À noter qu’une assertion inatteignable est toujours prouvée comme vraie de cette manière :Assertion que l'on saute par un Goto

Et c’est également le cas lorsque l’on sait trivialement qu’une instruction produit nécessairement une erreur d’exécution (par exemple en déréférençant la valeur NULL), comme nous avions déjà pu le constater avec l’exemple de l’appel à abs avec la valeur INT_MIN.

Pour prouver la terminaison d’une boucle, nous utilisons la notion de variant de boucle. Le variant de boucle n’est pas une propriété mais une valeur. C’est une expression faisant intervenir des éléments modifiés par la boucle et donnant une borne supérieure sur le nombre d’itérations restant à effectuer à un tour de la boucle. C’est donc une expression supérieure à 0 et strictement décroissante d’un tour de boucle à l’autre (cela sera également vérifié par induction par WP).

Si nous reprenons notre programme précédent, nous pouvons ajouter le variant de cette façon :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
int main(){
  int i = 0;
  int h = 42;

  /*@
    loop invariant 0 <= i <= 30;
    loop assigns i;
    loop variant 30 - i;
  */
  while(i < 30){
    ++i;
  }
  //@assert i == 30;
  //@assert h == 42;
}

Une nouvelle fois nous pouvons regarder les buts générés :

Notre simple boucle complètement spécifiée et prouvée

Le variant nous génère bien deux obligations au niveau de la vérification : assurer que la valeur est positive, et assurer qu’elle décroît strictement pendant l’exécution de la boucle. Et si nous supprimons la ligne de code qui incrémentei, WP ne peut plus prouver que la valeur 30 - i décroît strictement.

Il est également bon de noter qu’être capable de donner un variant de boucle n’induit pas nécessairement d’être capable de donner le nombre exact d’itérations qui doivent encore être exécutées par la boucle, car nous n’avons pas toujours une connaissance aussi précise du comportement de notre programme. Nous pouvons par exemple avoir un code comme celui-ci :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
#include <stddef.h>

/*@
  ensures min <= \result <= max;
*/
size_t random_between(size_t min, size_t max);

void undetermined_loop(size_t bound){
  /*@
    loop invariant 0 <= i <= bound ;
    loop assigns i;
    loop variant i;
   */
  for(size_t i = bound; i > 0; ){
    i -= random_between(1, i);
  }
}

Ici, à chaque tour de boucle, nous diminuons la valeur de la variable i par une valeur dont nous savons qu’elle se trouve entre 1 et i. Nous pouvons donc bien assurer que la valeur de i est positive et décroît strictement, mais nous ne pouvons pas dire combien de tours de boucles vont être réalisés pendant une exécution.

Le variant n’est donc bien qu’une borne supérieure sur le nombre d’itérations de la boucle.

Lier la post-condition et l’invariant

Supposons le programme spécifié suivant. Notre but est de prouver que le retour de cette fonction est l’ancienne valeur de a à laquelle nous avons ajouté 10.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
/*@
    ensures \result == \old(a) + 10;
*/
int plus_dix(int a){
    /*@
        loop invariant 0 <= i <= 10;
        loop assigns i, a;
        loop variant 10 - i;
    */
    for (int i = 0; i < 10; ++i)
        ++a;

    return a;
}

Le calcul de plus faibles pré-conditions ne permet pas de sortir de la boucle des informations qui ne font pas partie de l’invariant. Dans un programme comme :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
/*@
    ensures \result == \old(a) + 10;
*/
int plus_dix(int a){
    ++a;
    ++a;
    ++a;
    //...
    return a;
}

En remontant les instructions depuis la post-condition, on conserve toujours les informations à propos de a. À l’inverse, comme mentionné plus tôt, en dehors de la boucle WP ne considérera que les informations fournies par notre invariant. Par conséquent, notre fonction plus_dix ne peut pas être prouvée en l’état : l’invariant ne mentionne rien à propos de a. Pour lier notre post-condition à l’invariant, il faut ajouter une telle information. Par exemple :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
/*@
    ensures \result == \old(a) + 10;
*/
int plus_dix(int a){
    /*@
        loop invariant 0 <= i <= 10;
        loop invariant a = \old(a) + i; //< AJOUT
        loop assigns i, a;
        loop variant 10 - i;
    */
    for (int i = 0; i < 10; ++i)
        ++a;

    return a;
}

Ce besoin peut apparaître comme une contrainte très forte. Il ne l’est en fait pas tant que cela. Il existe des analyses fortement automatiques capables de calculer les invariants de boucles. Par exemple, sans spécifications, une interprétation abstraite calculera assez facilement 0 <= i <= 10 et \old(a) <= a <= \old(a)+10. En revanche, il est souvent bien plus difficile de calculer les relations qui existent entre des variables différentes qui évoluent dans le même programme, par exemple l’égalité mentionnée par notre invariant ajouté.

Les boucles - Exemples

Exemple avec un tableau read-only

S’il y a une structure de données que nous traitons avec les boucles c’est bien le tableau. C’est une bonne base d’exemples pour les boucles car ils permettent rapidement de présenter des invariants intéressants et surtout, ils vont nous permettre d’introduire des constructions très importantes d’ACSL.

Prenons par exemple la fonction qui cherche une valeur dans un tableau :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
#include <stddef.h>

/*@
  requires 0 < length;
  requires \valid_read(array + (0 .. length-1));

  assigns  \nothing;

  behavior in:
    assumes \exists size_t off ; 0 <= off < length && array[off] == element;
    ensures array <= \result < array+length && *\result == element;

  behavior notin:
    assumes \forall size_t off ; 0 <= off < length ==> array[off] != element;
    ensures \result == NULL;

  disjoint behaviors;
  complete behaviors;
*/
int* search(int* array, size_t length, int element){
  /*@
    loop invariant 0 <= i <= length;
    loop invariant \forall size_t j; 0 <= j < i ==> array[j] != element;
    loop assigns i;
    loop variant length-i;
  */ 
  for(size_t i = 0; i < length; i++)
    if(array[i] == element) return &array[i];
  return NULL;
}

Cet exemple est suffisamment fourni pour introduire des notations importantes.

D’abord, comme nous l’avons déjà mentionné, le prédicat \valid_read (de même que \valid) nous permet de spécifier non seulement la validité d’une adresse en lecture mais également celle de tout un ensemble d’adresses contiguës. C’est la notation que nous avons utilisée dans cette expression :

1
//@ requires \valid_read(a + (0 .. length-1));

Cette pré-condition nous atteste que les adresses a+0, a+1 …, a+length-1 sont valides en lecture.

Nous avons également introduit deux notations qui vont nous être très utiles, à savoir \forall ($\forall$) et \exists ($\exists$), les quantificateurs de la logique. Le premier nous servant à annoncer que pour tout élément, la propriété suivante est vraie. Le second pour annoncer qu’il existe un élément tel que la propriété est vraie. Si nous commentons les deux lignes en questions, nous pouvons les lire de cette façon :

1
2
3
4
5
6
7
8
9
/*@
//pour tout "off" de type "size_t", tel que SI "off" est compris entre 0 et "length"
//                                 ALORS la case "off" de "a" est différente de "element"
\forall size_t off ; 0 <= off < length ==> a[off] != element;

//il existe "off" de type "size_t", tel que "off" soit compris entre 0 et "length"
//                                 ET que la case "off" de "a" vaille "element"
\exists size_t off ; 0 <= off < length && a[off] == element;
*/

Si nous devions résumer leur utilisation, nous pourrions dire que sur un certain ensemble d’éléments, une propriété est vraie, soit à propos d’au moins l’un d’eux, soit à propos de la totalité d’entre eux. Un schéma qui reviendra typiquement dans ce cas est que nous restreindrons cet ensemble à travers une première propriété (ici : 0 <= off < length) puis nous voudrons prouver la propriété réelle qui nous intéresse à propos d’eux. Mais il y a une différence fondamentale entre l’usage de exists et celui de forall.

Avec \forall type a ; p(a) ==> q(a), la restriction (p) est suivie par une implication. Pour tout élément, s’il respecte une première propriété (p), alors vérifier la seconde propriété q. Si nous mettions un ET comme pour le « il existe » (que nous expliquerons ensuite), cela voudrait dire que nous voulons que tout élément respecte à la fois les deux propriétés. Parfois, cela peut être ce que nous voulons exprimer, mais cela ne correspond alors plus à l’idée de restreindre un ensemble dont nous voulons montrer une propriété particulière.

Avec \exists type a ; p(a) && q(a), la restriction (p) est suivie par une conjonction, nous voulons qu’il existe un élément tel que cet élément est dans un certain état (défini par p), tout en respectant l’autre propriété q. Si nous mettions une implication comme pour le « pour tout », alors une telle expression devient toujours vraie à moins que p soit une tautologie ! Pourquoi ? Existe-t-il « a » tel que p(a) implique q(a) ? Prenons n’importe quel « a » tel que p(a) est faux, l’implication devient vraie.

Cette partie de l’invariant mérite une attention particulière :

1
//@ loop invariant \forall size_t j; 0 <= j < i ==> array[j] != element;

En effet, c’est la partie qui définit l’action de notre boucle, elle indique à WP ce que la boucle va faire (ou apprendre dans le cas présent) tout au long de son exécution. Ici en l’occurrence, cette formule nous dit qu’à chaque tour, nous savons que pour toute case entre 0 et la prochaine que nous allons visiter (i exclue), elle stocke une valeur différente de l’élément recherché.

Le but de WP associé à la préservation de cet invariant est un peu compliqué, il n’est pour nous pas très intéressant de se pencher dessus. En revanche, la preuve de l’établissement de cet invariant est intéressante :

But trivial

Nous pouvons constater que cette propriété, pourtant complexe, est prouvée par Qed sans aucun problème. Si nous regardons sur quelles parties du programme la preuve se base, nous pouvons voir l’instruction i = 0 surlignée, et c’est bien la dernière instruction que nous effectuons sur i avant de commencer la boucle. Et donc effectivement, si nous faisons le remplacement dans la formule de l’invariant :

1
//@ loop invariant \forall size_t j; 0 <= j < 0 ==> array[j] != element;

« Pour tout j, supérieur ou égal à 0 et inférieur strict à 0 », cette partie est nécessairement fausse. Notre implication est donc nécessairement vraie.

Exemples avec tableaux mutables

Nous allons voir deux exemples avec la manipulation de tableaux en mutation. L’un avec une modification totale, l’autre en modification sélective.

Remise à zéro

Regardons la fonction effectuant la remise à zéro d’un tableau.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
#include <stddef.h>

/*@
  requires \valid(array + (0 .. length-1));
  assigns  array[0 .. length-1];
  ensures  \forall size_t i; 0 <= i < length ==> array[i] == 0;
*/
void raz(int* array, size_t length){
  /*@
    loop invariant 0 <= i <= length;
    loop invariant \forall size_t j; 0 <= j < i ==> array[j] == 0;
    loop assigns i, array[0 .. length-1];
    loop variant length-i;
  */
  for(size_t i = 0; i < length; ++i)
    array[i] = 0;
}

Les seules parties sur lesquelles nous pouvons nous attacher ici sont les assigns de la fonction et de la boucle. À nouveau, nous pouvons utiliser la notation n .. m pour indiquer les parties du tableau qui sont modifiées.

Chercher et remplacer

Le dernier exemple qui nous intéresse est l’algorithme « chercher et remplacer ». C’est donc un algorithme qui va sélectivement modifier des valeurs dans une certaine plage d’adresses. Il est toujours un peu difficile de guider l’outil dans ce genre de cas car, d’une part, nous devons garder « en mémoire » ce qui est modifié et ce qui ne l’est pas et, d’autre part, parce que l’induction repose sur ce fait.

À titre d’exemple, la première spécification que nous pouvons réaliser pour cette fonction ressemblerait à ceci :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
#include <stddef.h>

/*@
  requires \valid(array + (0 .. length-1));
  assigns array[0 .. length-1];

  ensures \forall size_t i; 0 <= i < length && \old(array[i]) == old
             ==> array[i] == new;
  ensures \forall size_t i; 0 <= i < length && \old(array[i]) != old 
             ==> array[i] == \old(array[i]);
*/
void search_and_replace(int* array, size_t length, int old, int new){
  /*@
    loop invariant 0 <= i <= length;
    loop invariant \forall size_t j; 0 <= j < i && \at(array[j], Pre) == old 
                     ==> array[j] == new;
    loop invariant \forall size_t j; 0 <= j < i && \at(array[j], Pre) != old 
                     ==> array[j] == \at(array[j], Pre);
    loop assigns i, array[0 .. length-1];
    loop variant length-i;
  */
  for(size_t i = 0; i < length; ++i){
    if(array[i] == old) array[i] = new;
  }
}

Nous utilisons la fonction logique \at(v, Label) qui nous donne la valeur de la variable v au point de programme Label. Si nous regardons l’utilisation qui en est faite ici, nous voyons que dans l’invariant de boucle, nous cherchons à établir une relation entre les anciennes valeurs du tableau et leurs potentielles nouvelles valeurs :

1
2
3
4
5
6
/*@
  loop invariant \forall size_t j; 0 <= j < i && \at(array[j], Pre) == old 
                   ==> array[j] == new;
  loop invariant \forall size_t j; 0 <= j < i && \at(array[j], Pre) != old 
                   ==> array[j] == \at(array[j], Pre);
*/

Pour tout élément que nous avons visité, s’il valait la valeur qui doit être remplacée, alors il vaut la nouvelle valeur, sinon il n’a pas changé. En fait, si nous essayons de prouver l’invariant, WP n’y parvient pas. Dans ce genre de cas, le plus simple est encore d’ajouter diverses assertions exprimant les propriétés intermédiaires que nous nous attendons à voir facilement prouvées et impliquant l’invariant. En fait, nous nous apercevons rapidement que WP n’arrive pas à maintenir le fait que nous n’avons pas encore modifié la fin du tableau :

1
2
3
4
for(size_t i = 0; i < length; ++i){
    //@assert array[i] == \at(array[i], Pre); // échec de preuve
    if(array[i] == old) array[i] = new;
}

Nous pouvons donc ajouter cette information comme invariant :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
/*@
  loop invariant 0 <= i <= length;
  loop invariant \forall size_t j; 0 <= j < i && \at(array[j], Pre) == old 
                   ==> array[j] == new;
  loop invariant \forall size_t j; 0 <= j < i && \at(array[j], Pre) != old 
                   ==> array[j] == \at(array[j], Pre);

  //La fin du tableau n'a pas été modifiée :
  loop invariant \forall size_t j; i <= j < length
                     ==> array[j] == \at(array[j], Pre);
  loop assigns i, array[0 .. length-1];
  loop variant length-i;
*/
for(size_t i = 0; i < length; ++i){
  if(array[i] == old) array[i] = new;
}

Et cette fois, la preuve passera. À noter que si nous tentons la preuve directement avec la vérification des RTE, il est possible qu’Alt-Ergo n’y parvienne pas (CVC4 décharge l’ensemble sans problème). Dans ce cas, nous pouvons faire séparément les deux preuves (sans, puis avec RTE) ou encore ajouter des assertions permettant de guider la preuve dans la boucle :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
for(size_t i = 0; i < length; ++i){
  if(array[i] == old) array[i] = new;

  /*@ assert \forall size_t j; i < j < length 
               ==> array[j] == \at(array[j], Pre);                      */
  /*@ assert \forall size_t j; 0 <= j <= i && \at(array[j], Pre) == old 
               ==> array[j] == new;                                     */
  /*@ assert \forall size_t j; 0 <= j <= i && \at(array[j], Pre) != old 
               ==> array[j] == \at(array[j], Pre);                      */    
}

À mesure que nous cherchons à prouver des propriétés plus compliquées et notamment dépendantes de boucles, il va y avoir une part de tâtonnement pour comprendre ce qui manque au prouveur pour réussir la preuve.

Ce qui peut lui manquer, ce sont des hypothèses. Dans ce type de cas, nous pouvons tenter d’ajouter des assertions au code pour guider le prouveur. Avec de l’expérience, nous pouvons regarder le contenu des obligations de preuve ou tenter de commencer la preuve avec Coq pour voir si la preuve semble réalisable. Parfois le prouveur manque juste de temps, auquel cas, il suffit d’augmenter (parfois de beaucoup) la durée du timeout. Finalement, la propriété peut également être hors de portée du prouveur. Auquel cas, il faudra écrire une preuve à la main avec un prouveur interactif.

Enfin, il reste le cas où l’implémentation est effectivement fausse, et dans ce cas, il faut la corriger. Et c’est là que nous utiliserons plutôt le test que la preuve, car le test permet de prouver la présence d’un bug. ;)


Dans cette partie nous avons pu voir comment se traduisent les affectations et les structures de contrôle d’un point de vue logique. Nous nous sommes beaucoup attardés sur les boucles parce que c’est là que se trouvent la majorité des difficultés lorsque nous voulons spécifier et prouver un programme par vérification déductive, les annotations ACSL qui leur sont spécifiques nous permettent d’exprimer le plus précisément possible leur comportement.

Pour la suite, nous allons nous attarder plus précisément sur les constructions que nous offre le langage ACSL du côté de la logique. Elles sont très importantes parce que ce sont elles qui vont nous permettre de nous abstraire du code pour avoir des spécifications plus compréhensibles et plus aisément prouvables.