Vérification formelle

Outils de preuve mathématique (McCarthy, Floyd, Hoare, Dijkstra)

Idée : on suppose qu’il existe dans un programme un certain nombre de points P₁, P₂, ..., P_n où le concepteur peut fournir des assertions a₁, a₂,...,a_n concernant les variables du programme et leurs relations. L’assertion a₁ concerne les entrées du programme, a_n ses sorties.

Pour prouver que les instructions du programme entre P_i et P_i+1 sont correctes, il faut démontrer que l’exécution de ces instructions transforme a_i en a_i+1.

Si les assertions d’entrée et de sortie sont correctement formulées et si le programme se termine, alors le programme est correct.

Exemple :

  { x = 5 } x := x + 1 { x = 6 }
  { z - 43 > y + 7 } x := z - 43 { x > y + 7 }
  { x + y > 3 } x := x + 1; y := y + 1 { x + y > 5 }

Règle d'inférence :
  {A1} I1 {A2}  ∧  {A2} I2 {A3}   ⇒  {A1} I1; I2 {A3}

Exemple :

  if cond then I1 else I2 endif

Règle d'inférence :
  {Pre ∧ cond} I1 {Post}  ∧  {Pre ∧ ¬cond} I2 {Post}
          ⇒
  {Pre} if cond then I1 else I2 endif {Post}

Exercice : quelle instruction est définie par cette règle de preuve ?

  {Pre ∧ cond} I {Pre}
        ⇒
  {Pre} ??? {Pre &and ¬cond}

Exercice : le code ci-dessous est supposé de représenter le tri fusion. Trouvez l’invariant de la boucle.

  i = 0; j = 0; k = 0;
  while (k <= 2*n-1) {
    if (a[i] < b[j]){
      c[k] = a[i];
      i = i+1;
    } else {
      c[k] = b[j];
      j = j+1;
    }
    k = k+1;
  }

Preuves de correction dans la pratique

Objections soulevées :

• Preuves formelles sont souvent plus longues et plus complexes que les programmes prouvés. Alors, la preuve n’augmente pas notre confiance à ce que le programme est correct.
• Preuves formelles exigent trop de connaissances mathématiques pour un ingénieur logiciel moyen.
• Trop de détails techniques qui peuvent être évités dans une technique moins formelle.
• On ne peut jamais avoir confiance à 100%. Des pannes du matériel ou des erreurs dans un compilateur sont toujours possibles.
• Il est difficile de traiter des limites du matériel dans les preuves. Par exemple, le nombre de bits utilisés pour représenter des nombres réels.

Il est vrai que "preuves formelles sont souvent plus longues et plus complexes que les programmes prouvés". C’est la raison pour laquelle ces techniques devraient être appliquées de façon modulaire et incrémentale.

Outils d'analyse statique

• des outils qui analysent le texte source de programmes
• constituent un supplément à l'inspection
• très utiles dans le cas des langages avec un typage faible (C par exemple)

Exécution symbolique

Le rêve  (selon Symbolic Execution and Test-input Generation par W. Visser, C. Pasareanu, P. Mehlitz; NASA Ames Research Center) :

Exemple :

read(a);
read(b);
x = a+1;
y = x*b;
write(y);
/* (A+1)*B */

Exemple :

{true}
read(a);
x = a*a;
x = x+1;
write(x);
{sortie > 0}

Exemple :

public static void f(int N){
  int x = 0; int y = 0;
  while (x < N){
    x++; y++;
  }
  while (x != 0){
    x--; y--;
  }
  assert(y == 0);
}

Exemple (voir Symbolic Execution and Test-input Generation par W. Visser, C. Pasareanu, P. Mehlitz; NASA Ames Research Center) :

Model checking :
(voir Symbolic Execution and Test-input Generation par W. Visser, C. Pasareanu, P. Mehlitz; NASA Ames Research Center)

Le Model Checking désigne une famille de techniques de vérification automatique des systèmes informatiques (logiciels, circuits logiques, protocoles de communication). Il s'agit de tester algorithmiquement si un modèle donné, le système lui-même ou une abstraction du système, satisfait une spécification logique, généralement formulée en termes de logique temporelle.

Exemples d'erreurs qui peuvent être détectées par des outils d'analyse statique

• utilisation de variables avant leur déclaration
• variables jamais utilisées
• deux affectations consécutives pour une même variable sans son utilisation entre les deux
• code non-atteignable
• boucles infinies
• division par zéro