Licence CC BY-NC-SA

ACSL - Propriétés

Dernière mise à jour :

Depuis le début de ce tutoriel, nous avons vu divers prédicats et fonctions logiques qui sont fournis par défaut en ACSL : \valid, \valid_read, \separated, \old et \at. Il en existe bien sûr d’autres mais nous n’allons pas les présenter un à un, le lecteur pourra se référer à la documentation (ACSL implementation) pour cela (à noter : tout n’est pas nécessairement supporté par WP).

ACSL nous permet de faire plus que « simplement » spécifier notre code. Nous pouvons définir nos propres prédicats, fonctions, relations, etc. Le but est de pouvoir abstraire nos spécifications. Cela nous permet de les factoriser (par exemple en définissant ce qu’est un tableau valide), ce qui a deux effets positifs pour nous : d’abord nos spécifications deviennent plus lisibles donc plus faciles à comprendre, mais cela permet également de réutiliser des preuves déjà faites et donc de faciliter la preuve de nouveaux programmes.

Types primitifs supplémentaires

ACSL nous propose deux types qui vont nous permettre d’écrire des propriétés ou des fonctions sans avoir à se préoccuper des contraintes dues à la taille en mémoire des types primitifs du C. Ces types sont integer et real, qui représentent respectivement les entiers mathématiques et les réels mathématiques (pour ces derniers, la modélisation est aussi proche que possible de la réalité, mais la notion de réel ne peut pas être parfaitement représentée).

Par la suite, nous utiliserons souvent des entiers à la place des classiques ìnt du C. La raison est simplement que beaucoup de propriété sont vraies quelle que soit la taille de l’entier (au sens C, cette fois) en entrée.

En revanche, nous ne parlerons pas de real VS float/double, parce que cela induirait que nous parlions de preuve de programmes avec du calcul en virgule flottante et que nous n’en parlerons pas ici. Par contre, ce tutoriel en cours d’écriture en parle : effectuer des calculs numériques précis.

Prédicats

Un prédicat est une propriété portant sur des objets et pouvant être vraie ou fausse. En résumé, des prédicats, c’est ce que nous écrivons depuis le début de ce tutoriel dans les clauses de nos contrats et de nos invariants de boucle. ACSL nous permet de créer des versions nommées de ces prédicats, à la manière d’une fonction booléenne en C par exemple. À la différence près tout de même que les prédicats (ainsi que les fonctions logiques que nous verrons par la suite) doivent être pures, c’est-à-dire qu’elles ne peuvent pas produire d’effets de bords en modifiant des valeurs pointées par exemple.

Ces prédicats peuvent prendre un certain nombre de paramètres. En plus de cela, ils peuvent également recevoir un certain nombre de labels (au sens C du terme) qui vont permettre d’établir des relations entre divers points du code.

Syntaxe

Les prédicats sont, comme les spécifications, introduits au travers d’annotations. La syntaxe est la suivante :

1
2
3
4
/*@
  predicate nom_du_predicat { Label0, Label1, ..., LabelN }(type0 arg0, type1 arg1, ..., typeN argN) =
    //une relation logique entre toutes ces choses.
*/

Nous pouvons par exemple définir le prédicat nous disant qu’un entier en mémoire n’a pas changé entre deux points particuliers du programme :

1
2
3
4
/*@
  predicate unchanged{L0, L1}(int* i) =
    \at(*i, L0) == \at(*i, L1);
*/

Gardez bien en mémoire que le passage se fait, comme en C, par valeur. Nous ne pouvons pas écrire ce prédicat en passant directement i :

1
2
3
4
/*@
  predicate unchanged{L0, L1}(int i) =
    \at(i, L0) == \at(i, L1);
 */

Car i est juste une copie de la variable reçue en paramètre.

Nous pouvons par exemple vérifier ce petit code :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
int main(){
  int i = 13;
  int j = 37;

 Begin:
  i = 23;

  //@assert ! unchanged{Begin, Here}(&i);
  //@assert   unchanged{Begin, Here}(&j);
}

Nous pouvons également regarder les buts générés par WP et constater que, même s’il subit une petite transformation syntaxique, le prédicat n’est pas déroulé par WP. Ce sera au prouveur de déterminer s’il veut raisonner avec.

Comme nous l’avons dit plus tôt, une des utilités des prédicats et fonctions (que nous verrons un peu plus tard) est de rendre plus lisible nos spécifications et de les factoriser. Un exemple est d’écrire un prédicat pour la validité en lecture/écriture d’un tableau sur une plage particulière. Cela nous évite d’avoir à réécrire l’expression en question qui est moins compréhensible au premier coup d’œil.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
/*@
  predicate valid_range_rw(int* t, integer n) =
    n >= 0 && \valid(t + (0 .. n-1));

  predicate valid_range_ro(int* t, integer n) =
    n >= 0 && \valid_read(t + (0 .. n-1));
*/

/*@
  requires 0 < length;
  requires valid_range_ro(array, length);
  //...
*/
int* search(int* array, size_t length, int element)

Dans cette portion de spécification, le label pour les prédicats n’est pas précisé, ni pour leur création, ni pour leur utilisation. Pour la création, Frama-C va automatiquement en ajouter un dans la définition du prédicat. Pour l’appel, le label passé sera implicitement Here. La non-déclaration du label dans la définition n’interdit pour autant pas de passer explicitement un label lors de l’appel.

Bien entendu, les prédicats peuvent être déclarés dans des fichiers headers afin de produire une bibliothèque d’utilitaires de spécifications par exemple.

Abstraction

Une autre utilité importante des prédicats est de définir l’état logique de nos structures quand les programmes se complexifient. Nos structures doivent généralement respecter un invariant (encore) que chaque fonction de manipulation devra maintenir pour assurer que la structure sera toujours utilisable et qu’aucune fonction ne commettra de bavure.

Cela permet notamment de faciliter la lecture de spécifications. Par exemple, nous pourrions poser les spécifications nécessaires à la sûreté d’une pile de taille limitée. Et cela donnerait quelque chose comme :

 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
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
struct stack_int{
  size_t top;
  int    data[MAX_SIZE];
};

/*@
  predicate valid_stack_int(struct stack_int* s) = // à définir ;
  predicate empty_stack_int(struct stack_int* s) = // à définir ;
  predicate full_stack_int(struct stack_int* s) =  // à définir ;
*/

/*@
  requires \valid(s);
  assigns *s;
  ensures valid_stack_int(s) && empty_stack_int(s);
*/
void initialize(struct stack_int* s);

/*@
  requires valid_stack_int(s) && !full_stack_int(s);
  assigns  *s;
  ensures valid_stack_int(s);
*/
void push(struct stack_int* s, int value);

/*@
  requires valid_stack_int(s) && !empty_stack_int(s);
  assigns \nothing;
*/
int  top(struct stack_int* s);

/*@
  requires valid_stack_int(s) && !empty_stack_int(s);
  assigns *s;
  ensures valid_stack_int(s);
*/
void pop(struct stack_int* s);

/*@
  requires valid_stack_int(s);
  assigns \nothing;
  ensures \result == 1 <==> empty_stack_int(s);
*/
int  is_empty(stack_int_t s);


/*@
  requires valid_stack_int(s);
  assigns \nothing;
  ensures \result == 1 <==> full_stack_int(s);
*/
int  is_full(stack_int_t s);

Ici la spécification n’exprime pas de propriétés fonctionnelles. Par exemple, rien ne nous spécifie que lorsque nous faisons un push d’une valeur puis que nous demandons top, nous auront effectivement cette valeur. Mais elle nous donne déjà tout ce dont nous avons besoin pour produire un code où, à défaut d’avoir exactement les résultats que nous attendons (des comportements tels que « si j’empile une valeur $v$, l’appel à top renvoie la valeur $v$ », par exemple), nous pouvons au moins garantir que nous n’avons pas d’erreur d’exécution (à condition de poser une spécification correcte pour nos prédicats et de prouver les fonctions d’utilisation de la structure).

Fonctions logiques

Les fonctions logiques nous permettent de décrire des fonctions qui ne seront utilisables que dans les spécifications. Cela nous permet, d’une part, de les factoriser, et d’autre part de définir des opérations sur les types integer et real qui ne peuvent pas déborder contrairement aux types machines.

Comme les prédicats, elles peuvent recevoir divers labels et valeurs en paramètre.

Syntaxe

Pour déclarer une fonction logique, l’écriture est la suivante :

1
2
3
4
/*@
  logic type_retour ma_fonction{ Label0, ..., LabelN }( type0 arg0, ..., typeN argN ) =
    formule mettant en jeu les arguments ;
*/

Nous pouvons par exemple décrire une fonction affine générale du côté de la logique :

1
2
3
4
/*@
  logic integer ax_b(integer a, integer x, integer b) =
    a * x + b;
*/

Elle peut nous servir à prouver le code de la fonction suivante :

1
2
3
4
5
6
7
/*@ 
  assigns \nothing ;
  ensures \result == ax_b(3,x,4); 
*/
int function(int x){
  return 3*x + 4;
}
Les débordements semblent pouvoir survenir

Le code est bien prouvé mais les contrôles d’overflow, eux, ne le sont pas. Nous pouvons à nouveau définir des fonctions logiques générales, qui vont, du point de vue de la logique, nous fournir les bornes en fonction des valeurs que nous donnons en entrée. Cela nous permet ensuite d’ajouter nos contrôles de bornes en pré-condition de fonction :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
16
17
18
19
20
/*@
  logic integer limit_int_min_ax_b(integer a, integer b) =
    (a == 0) ? (b > 0) ? INT_MIN : INT_MIN-b :
    (a <  0) ? (INT_MAX-b)/a :
               (INT_MIN-b)/a ;

  logic integer limit_int_max_ax_b(integer a, integer b) =
    (a == 0) ? (b > 0) ? INT_MAX-b : INT_MAX :
    (a <  0) ? (INT_MIN-b)/a :
               (INT_MAX-b)/a ;
*/

/*@
  requires limit_int_min_ax_b(3,4) < x < limit_int_max_ax_b(3,4);
  assigns \nothing ;
  ensures \result == ax_b(3,x,4);
*/
int function(int x){
  return 3*x + 4;
}

Notons que comme dans la spécification, les calculs sont effectués à l’aide d’entiers mathématiques, nous n’avons pas à nous préoccuper d’un quelconque risque de débordement avec les calculs de INT_MIN-b ou INT_MAX-b.

Et cette fois tout est prouvé. Évidemment, nous pourrions fixer ces valeurs en dur chaque fois que nous avons besoin d’une nouvelle fonction affine du côté de la logique mais en posant ces fonctions, nous obtenons directement ces valeurs sans avoir besoin de les calculer nous même, ce qui est assez confortable.

Récursivité et limites

Les fonctions logiques peuvent être définie récursivement. Cependant, une telle définition va très rapidement montrer ses limites pour la preuve. En effet, pendant les manipulations des prouveurs automatiques sur les propriétés logiques, si l’usage d’une telle fonction est présente, elle devra être évaluée, or les prouveurs ne sont pas conçus pour faire ce genre d’évaluation qui se révélera donc généralement très coûteuse, produisant alors des temps de preuve trop longs menant à des timeouts.

Exemple concret, nous pouvons définir la fonction factorielle, dans la logique et en C :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
/*@
  logic integer factorial(integer n) = (n <= 0) ? 1 : n * factorial(n-1);
*/

/*@ 
  assigns \nothing ;
  ensures \result == factorial(n) ; 
*/
unsigned facto(unsigned n){
  return (n == 0) ? 1 : n * facto(n-1);
}

Sans contrôle de borne, cette fonction se prouve rapidement. Si nous ajoutons le contrôle des RTE, le vérification de débordement sur l’entier non-signé n’est pas ajoutée, car c’est un comportement déterminé d’après la norme C. Pour ajouter une assertion à ce point, nous pouvons demander à WP de générer ses propres vérifications en faisant un clic droit sur la fonction puis « insert WP-safety guards ». Et dans ce cas, le non-débordemement n’est pas prouvé.

Sur le type unsigned, le maximum que nous pouvons calculer est la factorielle de 12. Au-delà, cela produit un dépassement. Nous pouvons donc ajouter cette pré-condition :

1
2
3
4
5
6
7
8
/*@ 
  requires n <= 12 ;
  assigns \nothing ;
  ensures \result == factorial(n) ; 
*/
unsigned facto(unsigned n){
  return (n == 0) ? 1 : n * facto(n-1);
}

Si nous demandons la preuve avec cette entrée, Alt-ergo échouera pratiquement à coup sûr. En revanche, le prouveur Z3 produit la preuve en moins d’une seconde. Parce que dans ce cas précis, les heuristiques de Z3 considèrent que c’est une bonne idée de passer un peu plus de temps sur l’évaluation de la fonction. Nous pouvons par exemple changer la valeur maximale de n pour voir comment se comporte les différents prouveurs. Avec un n maximal fixé à 9, Alt-ergo produit la preuve en moins de 10 secondes, tandis que pour une valeur à 10, même une minute ne suffit pas.

Les fonctions logiques peuvent donc être définies récursivement mais sans astuces supplémentaires, nous venons vite nous heurter au fait que les prouveurs vont au choix devoir faire de l’évaluation, ou encore « raisonner » par induction, deux tâches pour lesquelles ils ne sont pas du tout fait, ce qui limite nos possibilités de preuve.

Lemmes

Les lemmes sont des propriétés générales à propos des prédicats ou encore des fonctions. Une fois ces propriétés exprimées, la preuve peut être réalisée une fois et la propriété en question pourra être utilisée par les prouveurs, leur permettant ainsi de ne pas reproduire les étapes de preuve nécessaires à chaque fois qu’une propriété équivalente intervient dans une preuve plus longue sur une propriété plus précise.

Les lemmes peuvent par exemple nous permettre d’exprimer des propriétés à propos des fonctions récursives pour que les preuves les faisant intervenir nécessitent moins de travail pour les prouveurs.

Syntaxe

Une nouvelle fois, nous les introduisons à l’aide d’annotations ACSL. La syntaxe utilisée est la suivante :

1
2
3
4
/*@
  lemma name_of_the_lemma { Label0, ..., LabelN }:
    property ;
*/

Cette fois les propriétés que nous voulons exprimer ne dépendent pas de paramètres reçus (hors de nos labels bien sûr). Ces propriétés seront donc exprimées sur des variables quantifiées. Par exemple, nous pouvons poser ce lemme qui est vrai, même s’il est trivial :

1
2
3
4
/*@
  lemma lt_plus_lt:
    \forall integer i, j ; i < j ==> i+1 < j+1;
*/

Cette preuve peut être effectuée en utilisant WP. La propriété est bien sûr trivialement prouvée par Qed.

Exemple : propriété fonction affine

Nous pouvons par exemple reprendre nos fonctions affines et exprimer quelques propriétés intéressantes à leur sujet :

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
/* @
  lemma ax_b_monotonic_neg:
    \forall integer a, b, i, j ;
      a <  0 ==> i <= j ==> ax_b(a, i, b) >= ax_b(a, j, b);
  lemma ax_b_monotonic_pos:
    \forall integer a, b, i, j ;
      a >  0 ==> i <= j ==> ax_b(a, i, b) <= ax_b(a, j, b);
  lemma ax_b_monotonic_nul:
    \forall integer a, b, i, j ;
      a == 0 ==> ax_b(a, i, b) == ax_b(a, j, b);
*/

Pour ces preuves, il est fort possible qu’Alt-ergo ne parvienne pas à les décharger. Dans ce cas, le prouveur Z3 devrait, lui, y arriver. Nous pouvons ensuite construire cet exemple de code :

 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
/*@
  requires a > 0;
  requires limit_int_min_ax_b(a,4) < x < limit_int_max_ax_b(a,4);
  assigns \nothing ;
  ensures \result == ax_b(a,x,4);
*/
int function(int a, int x){
  return a*x + 4;
}

/*@ 
  requires a > 0;
  requires limit_int_min_ax_b(a,4) < x < limit_int_max_ax_b(a,4) ;
  requires limit_int_min_ax_b(a,4) < y < limit_int_max_ax_b(a,4) ;
  assigns \nothing ;
*/
void foo(int a, int x, int y){
  int fmin, fmax;
  if(x < y){
    fmin = function(a,x);
    fmax = function(a,y);
  } else {
    fmin = function(a,y);
    fmax = function(a,x);
  }
  //@assert fmin <= fmax;
}

Si nous ne renseignons pas les lemmes mentionnés plus tôt, il y a peu de chances qu’Alt-ergo réussisse à produire la preuve que fmin est inférieur à fmax. Avec ces lemmes présents en revanche, il y parvient sans problème car cette propriété est une simple instance du lemme ax_b_monotonic_pos, la preuve étant ainsi triviale car notre lemme nous énonce cette propriété comme étant vraie.


Dans cette partie, nous avons vu les constructions de ACSL qui nous permettent de factoriser un peu nos spécifications et d’exprimer des propriétés générales pouvant être utilisées par les prouveurs pour faciliter leur travail.

Toutes les techniques expliquées dans cette partie sont sûres, au sens où elles ne permettent a priori pas de fausser la preuve avec des définitions fausses ou contradictoires. En tous cas, si la spécification n’utilise que ce type de constructions et que chaque lemme, chaque pré-condition (aux points d’appels), chaque post-condition, chaque assertion, chaque variant et chaque invariant est correctement prouvé, le code est juste.

Parfois ces constructions ne sont pas suffisantes pour exprimer toutes nos propriétés ou pour prouver nos programmes. Les prochaines constructions que nous allons voir vont nous ajouter de nouvelles possibilités à ce sujet, mais il faudra se montrer prudent dans leur usage car des erreurs pourraient nous permettre de créer des hypothèses fausses ou d’altérer le programme que nous vérifions.