Licence CC BY-NC-SA

ACSL - Définitions logiques et code

Dernière mise à jour :

Dans cette partie nous allons voir deux notions importantes d’ACSL :

  • les définitions axiomatiques,
  • le code fantôme.

Dans certaines configurations, ces deux notions sont absolument nécessaires pour faciliter le processus de spécification et de preuve. Soit en forçant l’abstraction de certaines propriétés, soit en explicitant des informations qui sont autrement implicites et plus difficiles à prouver.

Le risque de ces deux notions est qu’elles peuvent rendre notre preuve inutile si nous faisons une erreur dans leur usage. La première en nous autorisant à introduire des hypothèses fausses ou des définitions trop imprécises. La seconde en nous ouvrant le risque de modifier le programme vérifié, nous faisant ainsi prouver un autre programme que celui que nous voulons prouver.

Définitions axiomatiques

Les axiomes sont des propriétés dont nous énonçons qu’elles sont vraies quelle que soit la situation. C’est un moyen très pratique d’énoncer des notions complexes qui vont pouvoir rendre le processus très efficace en abstrayant justement cette complexité. Évidemment, comme toute propriété exprimée comme un axiome est supposée vraie, il faut également faire très attention à ce que nous définissons car si nous introduisons une propriété fausse dans les notions que nous supposons vraies alors … nous saurons tout prouver, même ce qui est faux.

Syntaxe

Pour introduire une définition axiomatique, nous utilisons la syntaxe suivante :

/*@
  axiomatic Name_of_the_axiomatic_definition {
    // ici nous pouvons définir ou déclarer des fonctions et prédicats

    axiom axiom_name { Label0, ..., LabelN }:
      // property ;

    axiom other_axiom_name { Label0, ..., LabelM }:
      // property ;

    // ... nous pouvons en mettre autant que nous voulons
  }
*/

Nous pouvons par exemple définir cette axiomatique :

/*@
  axiomatic lt_plus_lt{
    axiom always_true_lt_plus_lt:
      \forall integer i, j; i < j ==> i+1 < j+1 ;
  }
*/

Et nous pouvons voir que dans Frama-C, la propriété est bien supposée vraie :

Premier axiome, supposé vrai par Frama-C
Premier axiome, supposé vrai par Frama-C

Actuellement nos prouveurs automatiques n’ont pas la puissance nécessaire pour calculer la réponse à la grande question sur la vie, l’univers et le reste. Qu’à cela ne tienne nous pouvons l’énoncer comme axiome ! Reste à comprendre la question pour savoir où ce résultat peut-être utile …

/*@
  axiomatic Ax_answer_to_the_ultimate_question_of_life_the_universe_and_everything {
    logic integer the_ultimate_question_of_life_the_universe_and_everything{L} ;

    axiom answer{L}:
      the_ultimate_question_of_life_the_universe_and_everything{L} = 42;
  }
*/

Lien avec la notion de lemme

Les lemmes et les axiomes vont nous permettre d’exprimer les mêmes types de propriétés, à savoir des propriétés exprimées sur des variables quantifiées (et éventuellement des variables globales, mais cela reste assez rare puisqu’il est difficile de trouver une propriété qui soit globalement vraie à leur sujet tout en étant intéressante). Outre ce point commun, il faut également savoir que comme les axiomes, en dehors de leur définition, les lemmes sont considérés vrais par WP.

La seule différence entre lemme et axiome du point de vue de la preuve est donc que nous devrons fournir une preuve que le premier est valide alors que l’axiome est toujours supposé vrai.

Définition de fonctions ou prédicats récursifs

Les définitions axiomatiques de fonctions ou de prédicats récursifs sont particulièrement utiles car elles vont permettre d’empêcher les prouveurs de dérouler la récursion quand c’est possible.

L’idée est alors de ne pas définir directement la fonction ou le prédicat mais plutôt de la déclarer puis de définir des axiomes spécifiant son comportement. Si nous reprenons par exemple la factorielle, nous pouvons la définir axiomatiquement de cette manière :

/*@
  axiomatic Factorial{
    logic integer factorial(integer n);
    
    axiom factorial_0:
      \forall integer i; i <= 0 ==> 1 == factorial(i) ;

    axiom factorial_n:
      \forall integer i; i > 0 ==> i * factorial(i-1) == factorial(i) ;
  }
*/

Dans cette définition axiomatique, notre fonction n’a pas de corps. Son comportement étant défini par les axiomes ensuite définis.

Une petite subtilité est qu’il faut prendre garde au fait que si les axiomes énoncent des propriétés à propos du contenu d’une ou plusieurs zones mémoires pointées, il faut spécifier ces zones mémoires en utilisant la notation reads au niveau de la déclaration. Si nous oublions une telle spécification, le prédicat, ou la fonction, sera considéré comme énoncé à propos du pointeur et non à propos de la zone mémoire pointée. Une modification de celle-ci n’entraînera donc pas l’invalidation d’une propriété connue axiomatiquement.

Si par exemple, nous voulons définir qu’un tableau ne contient que des 0, nous pouvons le faire de cette façon :

/*@
  axiomatic A_all_zeros{
    predicate zeroed{L}(int* a, integer b, integer e) reads a[b .. e-1];

    axiom zeroed_empty{L}:
      \forall int* a, integer b, e; b >= e ==> zeroed{L}(a,b,e);
      
    axiom zeroed_range{L}:
      \forall int* a, integer b, e; b < e ==>
        zeroed{L}(a,b,e-1) && a[e-1] == 0 <==> zeroed{L}(a,b,e);
  }
*/

Et nous pouvons à nouveau prouver notre fonction de remise à zéro avec cette nouvelle définition :

#include <stddef.h>

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

Selon votre version de Frama-C et de vos prouveurs automatiques, la preuve de préservation de l’invariant peut échouer. Une raison à cela est que le prouveur ne parvient pas à garder l’information que ce qui précède la cellule en cours de traitement par la boucle est toujours à 0. Nous pouvons ajouter un lemme dans notre base de connaissance, expliquant que si l’ensemble des valeurs d’un tableau n’a pas changé, alors la propriété est toujours vérifiée :

/*@
  predicate same_elems{L1,L2}(int* a, integer b, integer e) =
    \forall integer i; b <= i < e ==> \at(a[i],L1) == \at(a[i],L2);

  lemma no_changes{L1,L2}:
  \forall int* a, integer b, e;
  same_elems{L1,L2}(a,b,e) ==> zeroed{L1}(a,b,e) ==> zeroed{L2}(a,b,e);
*/

Et d’énoncer une assertion pour spécifier ce qui n’a pas changé entre le début du bloc de la boucle (marqué par le label L dans le code) et la fin (qui se trouve être Here puisque nous posons notre assertion à la fin) :

for(size_t i = 0; i < length; ++i){
  L:
  array[i] = 0;
  //@ assert same_elems{L,Here}(array,0,i);
}

À noter que dans cette nouvelle version du code, la propriété énoncée par notre lemme n’est pas prouvée par les solveurs automatiques, qui ne savent pas raisonner pas induction. Pour les curieux, la (très simple) preuve en Coq est ci-dessous :

(* Généré par WP *)
Definition P_same_elems (Mint_0 : farray addr Z) (Mint_1 : farray addr Z)
    (a : addr) (b : Z) (e : Z) : Prop :=
    forall (i : Z), let a_1 := (shift_sint32 a i%Z) in ((b <= i)%Z) ->
      ((i < e)%Z) -> (((Mint_0.[ a_1 ]) = (Mint_1.[ a_1 ]))%Z).
Goal
  forall (i_1 i : Z), forall (t_1 t : farray addr Z), forall (a : addr),
    ((P_zeroed t a i_1%Z i%Z)) -> ((P_same_elems t_1 t a i_1%Z i%Z)) -> ((P_zeroed t_1 a i_1%Z i%Z)).
(* Notre preuve *)
Proof.
  intros b e.
  (* par induction sur la distance entre b et e *)
  induction e using Z_induction with (m := b) ; intros mem_l2 mem_l1 a Hz_l1 Hsame.
  (* cas de base : Axiome "empty" *)
  + apply A_A_all_zeros.Q_zeroed_empty ; assumption.
  + replace (e + 1) with (1 + e) in * ; try omega.
    (* on utilise l'axiome range *)
    rewrite A_A_all_zeros.Q_zeroed_range in * ; intros Hinf.
    apply Hz_l1 in Hinf ; clear Hz_l1 ; inversion_clear Hinf as [Hlast Hothers].
    split.
    (* sous plage de Hsame *)
    - rewrite Hsame ; try assumption ; omega.
    (* hypothèse d'induction *)
    - apply IHe with (t := mem_l1) ; try assumption.
      * unfold P_same_elems ; intros ; apply Hsame ; omega.
Qed.

Dans le cas présent, utiliser une axiomatique est contre-productif : notre propriété est très facilement exprimable en logique du premier ordre comme nous l’avons déjà fait précédemment. Les axiomatiques sont faites pour écrire des définitions qui ne sont pas simples à exprimer dans le formalisme de base d’ACSL. Mais il est mieux de commencer avec un exemple facile à lire.

Consistance

En ajoutant des axiomes à notre base de connaissances, nous pouvons produire des preuves plus complexes car certaines parties de cette preuve, mentionnées par les axiomes, ne nécessiteront plus de preuves qui allongeraient le processus complet. Seulement, en faisant cela nous devons être extrêmement prudents. En effet, la moindre hypothèse fausse introduite dans la base pourraient rendre tous nos raisonnements futiles. Notre raisonnement serait toujours correct, mais basé sur des connaissances fausses, il ne nous apprendrait donc plus rien de correct.

L’exemple le plus simple à produire est le suivant:

/*@
  axiomatic False{
    axiom false_is_true: \false;
  }
*/

int main(){
  // Exemples de propriétés prouvées

  //@ assert \false;
  //@ assert \forall integer x; x > x;
  //@ assert \forall integer x,y,z ; x == y == z == 42;
  return *(int*) 0;
}

Et tout est prouvé, y compris que le déréférencement de l’adresse 0 est OK :

Preuve de tout un tas de choses fausses
Preuve de tout un tas de choses fausses

Évidemment cet exemple est extrême, nous n’écririons pas un tel axiome. Le problème est qu’il est très facile d’écrire une axiomatique subtilement fausse lorsque nous exprimons des propriétés plus complexes, ou que nous commençons à poser des suppositions sur l’état global d’un système.

Quand nous commençons à créer de telles définitions, ajouter de temps en temps une preuve ponctuelle de « false » dont nous voulons qu’elle échoue permet de s’assurer que notre définition n’est pas inconsistante. Mais cela ne fait pas tout ! Si la subtilité qui crée le comportement faux est suffisamment cachée, les prouveurs peuvent avoir besoin de beaucoup d’informations autre que l’axiomatique elle-même pour être menés jusqu’à l’inconsistance, donc il faut toujours être vigilant !

Notamment parce que par exemple, la mention des valeurs lues par une fonction ou un prédicat défini axiomatiquement est également importante pour la consistance de l’axiomatique. En effet, comme mentionné précédemment, si nous n’exprimons pas les valeurs lues dans le cas de l’usage d’un pointeur, la modification d’une valeur du tableau n’invalide pas une propriété que l’on connaitrait à propos du contenu du tableau par exemple. Dans un tel cas, la preuve passe mais l’axiome n’exprimant pas le contenu, nous ne prouvons rien.

Par exemple, si nous reprenons l’exemple de mise à zéro, nous pouvons modifier la définition de notre axiomatique en retirant la mention des valeurs dont dépendent le prédicat : reads a[b .. e-1]. La preuve passera toujours mais n’exprimera plus rien à propos du contenu des tableaux considérés.

Exemple : comptage de valeurs

Dans cet exemple, nous cherchons à prouver qu’un algorithme compte bien les occurrences d’une valeur dans un tableau. Nous commençons par définir axiomatiquement la notion de comptage dans un tableau :

/*@
  axiomatic Occurrences_Axiomatic{
    logic integer l_occurrences_of{L}(int value, int* in, integer from, integer to)
      reads in[from .. to-1];

    axiom occurrences_empty_range{L}:
      \forall int v, int* in, integer from, to;
        from >= to ==> l_occurrences_of{L}(v, in, from, to) == 0;

    axiom occurrences_positive_range_with_element{L}:
      \forall int v, int* in, integer from, to;
        (from < to && in[to-1] == v) ==>
      l_occurrences_of(v,in,from,to) == 1+l_occurrences_of(v,in,from,to-1);

    axiom occurrences_positive_range_without_element{L}:
      \forall int v, int* in, integer from, to;
        (from < to && in[to-1] != v) ==>
      l_occurrences_of(v,in,from,to) == l_occurrences_of(v,in,from,to-1);
  }
*/

Nous avons trois cas à gérer :

  • la plage de valeur concernée est vide : le nombre d’occurrences est 0 ;
  • la plage de valeur n’est pas vide et le dernier élément est celui recherché : le nombre d’occurrences est : le nombre d’occurrences dans la plage actuelle que l’on prive du dernier élément, plus 1 ;
  • la plage de valeur n’est pas vide et le dernier élément n’est pas celui recherché : le nombre d’occurrences est le nombre d’occurrences dans la plage privée du dernier élément.

Par la suite, nous pouvons écrire la fonction C exprimant ce comportement et la prouver :

/*@
  requires \valid_read(in+(0 .. length));
  assigns  \nothing;
  ensures  \result == l_occurrences_of(value, in, 0, length);
*/
size_t occurrences_of(int value, int* in, size_t length){
  size_t result = 0;
  
  /*@
    loop invariant 0 <= result <= i <= length;
    loop invariant result == l_occurrences_of(value, in, 0, i);
    loop assigns i, result;
    loop variant length-i;
  */
  for(size_t i = 0; i < length; ++i)
    result += (in[i] == value)? 1 : 0;

  return result;
}

Une alternative au fait de spécifier que dans ce code result est au maximum i est d’exprimer un lemme plus général à propos de la valeur du nombre d’occurrences, dont nous savons qu’elle est comprise entre 0 et la taille maximale de la plage de valeurs considérée :

/*@
lemma l_occurrences_of_range{L}:
  \forall int v, int* array, integer from, to:
    from <= to ==> 0 <= l_occurrences_of(v, a, from, to) <= to-from;
*/

La preuve de ce lemme ne pourra pas être déchargée par un solveur automatique. Il faudra faire cette preuve interactivement avec Coq par exemple. Exprimer des lemmes généraux prouvés manuellement est souvent une bonne manière d’ajouter des outils aux prouveurs pour manipuler plus efficacement les axiomatiques, sans ajouter formellement d’axiomes qui augmenteraient nos chances d’introduire des erreurs. Ici, nous devrons quand même réaliser les preuves des propriétés mentionnées.

Exemple : le tri

Nous allons prouver un simple tri par sélection :

size_t min_idx_in(int* a, size_t beg, size_t end){
  size_t min_i = beg;
  for(size_t i = beg+1; i < end; ++i)
    if(a[i] < a[min_i]) min_i = i;
  return min_i;
}

void swap(int* p, int* q){
  int tmp = *p; *p = *q; *q = tmp;
}

void sort(int* a, size_t beg, size_t end){
  for(size_t i = beg ; i < end ; ++i){
    size_t imin = min_idx_in(a, i, end);
    swap(&a[i], &a[imin]);
  }
}

Le lecteur pourra s’exercer en spécifiant et en prouvant les fonctions de recherche de minimum et d’échange de valeur. Nous cachons la correction ci-dessous et allons nous concentrer plutôt sur la spécification et la preuve de la fonction de tri qui sont une illustration intéressant de l’usage des axiomatiques.

/*@
  requires \valid_read(a + (beg .. end-1));
  requires beg < end;

  assigns  \nothing;

  ensures  \forall integer i; beg <= i < end ==> a[\result] <= a[i];
  ensures  beg <= \result < end;
*/
size_t min_idx_in(int* a, size_t beg, size_t end){
  size_t min_i = beg;

  /*@
    loop invariant beg <= min_i < i <= end;
    loop invariant \forall integer j; beg <= j < i ==> a[min_i] <= a[j];
    loop assigns min_i, i;
    loop variant end-i;
  */
  for(size_t i = beg+1; i < end; ++i){
    if(a[i] < a[min_i]) min_i = i;
  }
  return min_i;
}

/*@
  requires \valid(p) && \valid(q);
  assigns  *p, *q;
  ensures  *p == \old(*q) && *q == \old(*p);
*/
void swap(int* p, int* q){
  int tmp = *p; *p = *q; *q = tmp;
}

En effet, une erreur commune que nous pourrions faire dans le cas de la preuve du tri est de poser cette spécification (qui est vraie !) :

/*@
  predicate sorted(int* a, integer b, integer e) =
    \forall integer i, j; b <= i <= j < e ==> a[i] <= a[j];
*/

/*@
  requires \valid(a + (beg .. end-1));
  requires beg < end;
  assigns  a[beg .. end-1];
  ensures sorted(a, beg, end);
*/
void sort(int* a, size_t beg, size_t end){
  /*@ //annotation de l'invariant */
  for(size_t i = beg ; i < end ; ++i){
    size_t imin = min_idx_in(a, i, end);
    swap(&a[i], &a[imin]);
  }
}

Cette spécification est vraie. Mais si nous nous rappelons la partie concernant les spécifications, nous nous devons d’exprimer précisément ce que nous attendons. Avec la spécification actuelle, nous ne prouvons pas toutes les propriétés nécessaires d’un tri ! Par exemple, cette fonction remplit pleinement la spécification :

/*@
  requires \valid(a + (beg .. end-1));
  requires beg < end;

  assigns  a[beg .. end-1];
  
  ensures sorted(a, beg, end);
*/
void fail_sort(int* a, size_t beg, size_t end){
  /*@
    loop invariant beg <= i <= end;
    loop invariant \forall integer j; beg <= j < i ==> a[j] == 0;
    loop assigns i, a[beg .. end-1];
    loop variant end-i;
  */
  for(size_t i = beg ; i < end ; ++i)
    a[i] = 0;
}

En fait, notre spécification oublie que tous les éléments qui étaient originellement présents dans le tableau à l’appel de la fonction doivent toujours être présents après l’exécution de notre fonction de tri. Dit autrement, notre fonction doit en fait produire la permutation triée des valeurs du tableau.

Une propriété comme la définition de ce qu’est une permutation s’exprime extrêmement bien par l’utilisation d’une axiomatique. En effet, pour déterminer qu’un tableau est la permutation d’un autre, les cas sont très limités. Premièrement, le tableau est une permutation de lui-même, puis l’échange de deux valeurs sans changer les autres est également une permutation, et finalement si nous créons la permutation p2p_2 d’une permutation p1p_1, puis que nous créons la permutation p3p_3 de p2p_2, alors par transitivité p3p_3 est une permutation de p1p_1.

Ceci est exprimé par le code suivant :

/*@
  predicate swap_in_array{L1,L2}(int* a, integer b, integer e, integer i, integer j) =
    b <= i < e && b <= j < e &&
    \at(a[i], L1) == \at(a[j], L2) && \at(a[j], L1) == \at(a[i], L2) &&
    \forall integer k; b <= k < e && k != j && k != i ==> \at(a[k], L1) == \at(a[k], L2);

  axiomatic Permutation{
    predicate permutation{L1,L2}(int* a, integer b, integer e)
     reads \at(*(a+(b .. e - 1)), L1), \at(*(a+(b .. e - 1)), L2);

    axiom reflexive{L1}: 
      \forall int* a, integer b,e ; permutation{L1,L1}(a, b, e);

    axiom swap{L1,L2}:
      \forall int* a, integer b,e,i,j ;
        swap_in_array{L1,L2}(a,b,e,i,j) ==> permutation{L1,L2}(a, b, e);
    
    axiom transitive{L1,L2,L3}:
      \forall int* a, integer b,e ; 
        permutation{L1,L2}(a, b, e) && permutation{L2,L3}(a, b, e) ==> permutation{L1,L3}(a, b, e);
  }
*/

Nous spécifions alors que notre tri nous crée la permutation triée du tableau d’origine et nous pouvons prouver l’ensemble en complétant l’invariant de la fonction :

/*@
  requires beg < end && \valid(a + (beg .. end-1));
  assigns  a[beg .. end-1];  
  ensures sorted(a, beg, end);
  ensures permutation{Pre, Post}(a,beg,end);
*/
void sort(int* a, size_t beg, size_t end){
  /*@
    loop invariant beg <= i <= end;
    loop invariant sorted(a, beg, i) && permutation{Begin, Here}(a, beg, end);
    loop invariant \forall integer j,k; beg <= j < i ==> i <= k < end ==> a[j] <= a[k];
    loop assigns i, a[beg .. end-1];
    loop variant end-i;
  */
  for(size_t i = beg ; i < end ; ++i){
    //@ ghost begin: ;
    size_t imin = min_idx_in(a, i, end);
    swap(&a[i], &a[imin]);
    //@ assert swap_in_array{begin,Here}(a,beg,end,i,imin);
  }
}

Cette fois, notre propriété est précisément définie, la preuve reste assez simple à faire passer, ne nécessitant que l’ajout d’une assertion que le bloc de la fonction n’effectue qu’un échange des valeurs dans le tableau (et donnant ainsi la transition vers la permutation suivante du tableau). Pour définir cette notion d’échange, nous utilisons une annotation particulière (à la ligne 16), introduite par le mot-clé ghost. Ici, le but est d’introduire un label fictif dans le code qui est uniquement visible d’un point de vue spécification. C’est l’objet de la prochaine section.

Code Fantôme

Derrière ce titre faisant penser à un scénario de film d’action se cache en fait un moyen d’enrichir la spécification avec des informations sous la forme de code en langage C. Ici, l’idée va être d’ajouter des variables et du code source qui n’interviendra pas dans le programme réel mais permettant de créer des états logiques qui ne seront visibles que depuis la preuve. Par cet intermédiaire, nous pouvons rendre explicites des propriétés logiques qui étaient auparavant implicites.

Syntaxe

Le code fantôme est ajouté par l’intermédiaire d’annotations qui vont contenir du code C ainsi que la mention ghost.

/*@
  ghost
  // code en langage C
*/

Les seules règles que nous devons respecter dans un tel code est que nous ne devons jamais écrire une portion de mémoire qui n’est pas elle-même définie dans du code fantôme et que le code en question doit terminer tout bloc qu’il ouvrirait. Mis à par cela, tout calcul peut être inséré tant qu’il ne modifie que les variables du code fantôme.

Voici quelques exemples pour la syntaxe de code fantôme :

//@ ghost int ghost_glob_var = 0;

void foo(int a){
  //@ ghost int ghost_loc_var = a;

  //@ ghost Ghost_label: ;
  a = 28 ;

  //@ ghost if(a < 0){ ghost_loc_var = 0; }

  //@ assert ghost_loc_var == \at(a, Ghost_label) == \at(a, Pre);
}

Il faut être très prudent lorsque nous produisons ce genre de code. En effet, aucune vérification n’est effectuée pour s’assurer que nous n’écrivons pas dans la mémoire globale par erreur. Ce problème étant comme la vérification elle-même, un problème indécidable, une telle analyse serait un travail de preuve à part entière. Par exemple, ce code est accepté en entrée de Frama-C, alors qu’il modifie manifestement l’état de la mémoire du programme :

int a;

void foo(){
  //@ ghost a = 42;
}

Il faut donc faire très attention à ce que nous faisons avec du code fantôme.

Expliciter un état logique

Le but du code ghost est de rendre explicite des informations généralement implicites. Par exemple, dans la section précédente, nous nous en sommes servi pour récupérer explicitement un état logique connu à un point de programme donné.

Prenons maintenant un exemple plus poussé. Nous voulons par exemple prouver que la fonction suivante nous retourne la valeur maximale des sommes de sous-tableaux possibles d’un tableau donné. Un sous-tableau d’un tableau a est un sous-ensemble contigu de valeur de a. Par exemple, pour un tableau { 0 , 3 , -1 , 4 }, des exemples de sous tableaux peuvent être {}, { 0 }, { 3 , -1 } , { 0 , 3 , -1 , 4 }, … Notez que comme nous autorisons le tableau vide, la somme est toujours au moins égale à 0. Dans le tableau précédent, le sous tableau de valeur maximale est { 3 , -1 , 4 }, la fonction renverra donc 6.

int max_subarray(int *a, size_t len) {
  int max = 0;
  int cur = 0;
  for(size_t i = 0; i < len; i++) {
    cur += a[i];
    if (cur < 0)   cur = 0;
    if (cur > max) max = cur;
  }
  return max;
}

Pour spécifier la fonction précédente, nous allons avoir besoin d’exprimer axiomatiquement la somme. Ce n’est pas très complexe, et le lecteur pourra s’exercer en exprimant les axiomes nécessaires au bon fonctionnement de cette axiomatique :

/*@ axiomatic Sum {
  logic integer sum(int *array, integer begin, integer end) reads a[begin..(end-1)];
}*/

La correction est cachée ici :

/*@
  axiomatic Sum_array{
    logic integer sum(int* array, integer begin, integer end) reads array[begin .. (end-1)];
   
    axiom empty: 
      \forall int* a, integer b, e; b >= e ==> sum(a,b,e) == 0;
    axiom range:
      \forall int* a, integer b, e; b < e ==> sum(a,b,e) == sum(a,b,e-1)+a[e-1];
  }
*/

La spécification de notre fonction est la suivante :

/*@ 
  requires \valid(a+(0..len-1));
  assigns \nothing;
  ensures \forall integer l, h;  0 <= l <= h <= len ==> sum(a,l,h) <= \result;
  ensures \exists integer l, h;  0 <= l <= h <= len &&  sum(a,l,h) == \result;
*/

Pour toute paire de bornes, la valeur retournée par la fonction doit être supérieure ou égale à la somme des éléments entre les bornes, et il doit exister une paire de bornes, telle que la somme des éléments entre ces bornes est exactement la valeur retournée par la fonction. Par rapport à cette spécification, si nous devons ajouter les invariants de boucles, nous nous apercevons rapidement qu’il va nous manquer des informations. Nous avons besoin d’exprimer ce que sont les valeurs max et cur et quelles relations existent entre elles, mais rien ne nous le permet !

En substance, notre post-condition a besoin de savoir qu’il existe des bornes low et high telles que la somme calculée correspond à ces bornes. Or notre code, n’exprime rien de tel d’un point de vue logique et rien ne nous permet a priori de faire cette liaison en utilisant des formulations logiques. Nous allons donc utiliser du code ghost pour conserver ces bornes et exprimer l’invariant de notre boucle.

Nous allons d’abord avoir besoin de 2 variables qui vont nous permettre de stocker les valeurs des bornes de la plage maximum, nous les appellerons low et high. Chaque fois que nous trouverons une plage où la somme est plus élevée nous les mettrons à jour. Ces bornes correspondront donc à la somme indiquée par max. Cela induit que nous avons encore besoin d’une autre paire de bornes : celle correspondant à la variable de somme cur à partir de laquelle nous pourrons construire les bornes de max. Pour celle-ci, nous n’avons besoin que d’ajouter une variable ghost : le minimum actuel cur_low, la borne supérieure de la somme actuelle étant indiquée par la variable i de la boucle.

/*@ 
  requires \valid(a+(0..len-1));
  assigns \nothing;
  ensures \forall integer l, h;  0 <= l <= h <= len ==> sum(a,l,h) <= \result;
  ensures \exists integer l, h;  0 <= l <= h <= len &&  sum(a,l,h) == \result;
*/
int max_subarray(int *a, size_t len) {
  int max = 0;
  int cur = 0;
  //@ ghost size_t cur_low = 0; 
  //@ ghost size_t low = 0;
  //@ ghost size_t high = 0; 

  /*@ 
    loop invariant BOUNDS: low <= high <= i <= len && cur_low <= i;
    
    loop invariant REL :   cur == sum(a,cur_low,i) <= max == sum(a,low,high);
    loop invariant POST:   \forall integer l;    0 <= l <= i      ==> sum(a,l,i) <= cur;
    loop invariant POST:   \forall integer l, h; 0 <= l <= h <= i ==> sum(a,l,h) <= max;
   
    loop assigns i, cur, max, cur_low, low, high;
    loop variant len - i; 
  */
  for(size_t i = 0; i < len; i++) {
    cur += a[i];
    if (cur < 0) {
      cur = 0;
      /*@ ghost cur_low = i+1; */
    }
    if (cur > max) {
      max = cur;
      /*@ ghost low = cur_low; */
      /*@ ghost high = i+1; */
    }
  }
  return max;
}

L’invariant BOUNDS exprime comment sont ordonnées les différentes bornes pendant le calcul. L’invariant REL exprime ce que signifient les valeurs cur et max par rapport à ces bornes. Finalement, l’invariant POST permet de faire le lien entre les invariants précédents et la post-condition de la fonction.

Le lecteur pourra vérifier que cette fonction est effectivement prouvée sans la vérification des RTE. Si nous ajoutons également le contrôle des RTE, nous pouvons voir que le calcul de la somme indique un dépassement possible sur les entiers.

Ici, nous ne chercherons pas à le corriger car ce n’est pas l’objet de l’exemple. Le moyen de prouver cela dépend en fait fortement du contexte dans lequel on utilise la fonction. Une possibilité est de restreindre fortement le contrat en imposant des propriétés à propos des valeurs et de la taille du tableau. Par exemple : nous pourrions imposer une taille maximale et des bornes fortes pour chacune des cellules. Une autre possibilité est d’ajouter une valeur d’erreur en cas de dépassement (par exemple 1-1), et de spécifier qu’en cas de dépassement, c’est cette valeur qui est renvoyée.


Dans cette partie, nous avons vu des constructions plus avancées du langage ACSL qui nous permettent d’exprimer et de prouver des propriétés plus complexes à propos de nos programmes.

Mal utilisées, ces fonctionnalités peuvent fausser nos analyses, il faut donc se montrer attentif lorsque nous manipulons ces constructions et ne pas hésiter à les relire ou encore à exprimer des propriétés à vérifier à leur sujet afin de s’assurer que nous ne sommes pas en train d’introduire des incohérences dans notre programme ou nos hypothèses de travail.