Previous Up Next

Cours 8  Preuve de programmes impératifs

8.1  Logique de Hoare classique

On considère un langage PASCAL très simplifié, avec des variables globales entières, des expressions entières et booléennes, et les instructions d’affectation, de test et de boucle while :

e::=n ∣ x ∣ e  op  e
op::=+ ∣ − ∣ * ∣ / ∣ = ∣ ≠ ∣ < ∣ > ∣ ≤ ∣ ≥ ∣ and ∣ or 
i::=skip∣ x := e ∣ i ; i ∣ if  e  then  i  else  i ∣ while  e  do  i done
Exemple 5   Appelons ISQRT le programme suivant, sur trois variables n, count et sum :
count := 0; sum := 1;
while sum <= n do count := count + 1; sum := sum + 2 * count + 1 done
Affirmation : à la fin de l’exécution de ce programme, count est la racine carré de n, arrondie à l’entier inférieur.

8.1.1  Sémantique opérationnelle

Un état d’un programme est une table d’association E qui à chaque variable x du programme associe sa valeur courante E(x). La valeur d’une expression bien typée e dans un état E est définie par

E(n)=n 
E(x)=E(x)
E(e1 op e2)=E(e1)  op E(e2)

La sémantique opérationnelle de ce langage est définie par les règles de transition (sur toute instruction bien typée) :

E
 
x:=e
E{x=E(e)} 
E1
 
i1;i2
E3  si  E1 
 
i1
 E2  et E2 
 
i2
 E3 
E1
 
if e then i1 else i2
E2  si  E1(e)=true  et  E1 
 
i1
 E2 
E1
 
if e then i1 else i2
E2  si  E1(e)=false  et  E1 
 
i2
 E2 
E1
 
while e do i
E3  si  E1(e)=true, E1 
 
i
 E2  et  E2 
 
while e do i
 E3 
E
 
while e do i
E  si  E(e)=false

8.1.2  Logique de Hoare

Un triplet de Hoare est un triplet noté {P} i {Q} où P et Q sont des assertions logiques et i une instruction. Ces assertions logiques sont des formules du premier ordre, avec comme formules atomiques les expressions de notre langage. Remarque importante : il y a ainsi identification entre les variables du programme et les variables de la logique.

On dit qu’un triplet de Hoare {P} i {Q} est valide si pour tous états E1 et E2 tels que E1i E2 et P est vraie dans E1, Q est vraie dans E2.

Exemples de triplets valides : {x=1} x:=x+2 {x=3}, {x=y} x:=x+y {x=2y}.

Exemple 6   Sur le programme ISQRT, on souhaiterait montrer la validité du triplet
{n ≥ 0} ISQRT {count*count ≤ n ∧ n < (count+1)*(count+1)}

Logique de Hoare : ensemble de règles de déduction sur les triplets :

 
{Pskip {P}
 
{P∧ e=truei1 {Q}      {Pe=falsei2 {Q}
{Pif e then i1 else i2 {Q}
 
 
 
{P[x ← e]} x:=e {P}
 
{I∧ e=truei {I}
{Iwhile e do i {Ie=false}
 
 
 
{Pi1 {Q}      {Qi2 {R}
{Pi1;i2 {R}
 
{P′} i {Q′}     P → P′     Q′ → Q
{Pi {Q}
Proposition 1   Cet ensemble de règles est correct : tout triplet dérivable est valide.

Preuve : pas de difficulté (cf chapitre 2).

Difficulté : prouver un triplet à partir de ces règles demande de « deviner » les bonnes annotations intermédiaires, par exemple pour la séquence, mais aussi pour la règle d’affaiblissement. Ainsi, on ne peut pas prouver le programme de la racine carrée sans réfléchir : il faut en particulier trouver un invariant de boucle adéquat. L’équivalent, du point de vue théorique, de cette difficulté est : a-t-on complétude de la logique de Hoare, c.-à-d. peut-on prouver tous les triplets valides ?

8.1.3  Complétude, et calcul de plus faible précondition

Pour i et Q fixés, l’ensemble des P tels que {P} i {Q} est valide, s’il est non vide, possède-t-il un élément minimal P0 au sens où pour tout P tels que {P} i {Q} est valide, P implique P0.

Calcul de WP :

WP(x:=e,Q)=Q{x ← e
WP(i1;i2,Q)=WP(i1,WP(i2,Q)) 
WP(if e then i1 else i2,Q)=(e=true → WP(i1,Q))∧(e=false → WP(i2,Q)) 
WP(while e do i,Q)=pas de formule simple !
Exemple 7   WP(x:=x+y,x=2y) ≡ x+y=2y
Proposition 2   L’ensemble des règles de logique de Hoare est relativement complet : Tout triplet valide {P} i {Q} est dérivable (en particulier, on peut trouver des invariants pour les boucles while de i).

Preuve : le relativement exprime ici une hypothèse qui est que la logique dans laquelle on exprime les annotations est suffisamment expressive, en particulier pour exprimer les invariants de boucle nécessaires à l’aide de point-fixe [Cou90].

8.1.4  Difficultés

De nombreux travaux ont fait suite à la logique de Hoare originale [Cou90], pour étendre le formalisme et résoudre des difficultés, par exemple :

8.2  Transformation fonctionnelle : la méthode Why


 let isqrt =  fun (n : int) ->
  { n >= 0 }    (* pré-condition *)
   begin
     let count =  ref 0  in
     let sum =  ref 1  in
     begin
     while !sum <= n  do
      {  invariant count >= 0 and n >= count*count and sum = (count+1)*(count+1)
         variant   n - sum }  (* invariant et variant de boucle *)
      count := !count + 1;
      sum := !sum + 2 * !count + 1
     done;
    !count
     end
   end           
  {  result >= 0 and  result *  result <= n and n < ( result+1)*( result+1) }
    (* post-condition *)
Figure 8.1: Calcul de la racine carrée en Why

Objectif général : établir la validité d’un triplet de Hoare, non pas avec les règles de déduction précédente, mais avec une technique fondée sur le calcul des constructions inductives. Cet objectif a été développé par Jean-Christophe Filliâtre [Fil03a] et implantée dans un outil logiciel appelée Why [Fil03b]. Les programmes traités par Why ne sont pas en PASCAL, ni en C ou autre langage de programmation existant, mais dans une syntaxe spécifique, qui a été conçue pour la preuve de ces programmes.

En Why, toutes les difficultés mentionnées ci-dessus sont traitées, exceptés la possibilité d’avoir des structures de données complexes et les entiers bornés. Dans la section suivante, nous verrons à la fois comment traiter les structures de données complexes, et comment faire des preuves sur des programmes écrits dans des langages de programmation impératifs standards : Java ou C en l’occurrence.

La figure 8.1 donne de nouveau le programme qui calcule la racine carrée, écrit cette fois sous forme d’une fonction Why. On remarque que :


Figure 8.2: Approche multi-prouveur de Why

Le travail de l’outil Why consiste à produire, à partir d’un programme annoté, des obligations de preuves dont la validité assure la correction du programme. Avec Why, ces obligations de preuves sont des formules en logique du premier ordre, exprimable dans la syntaxe de différents démonstrateurs existants, aussi bien des démonstrateurs interactifs comme Coq, PVS, HOL-light ou Mizar, que des démonstrateurs automatiques comme Simplify ou haRVey.

Néanmoins, la sortie pour Coq possède une particularité supplémentaire : la validation, qui est un programme fonctionnel Coq équivalent au programme de départ. Il s’agit là de l’idée directrice de l’approche Why : un programme impératif peut être traduit en un programme fonctionnel par ajout de paramètre. Sur l’exemple de ISQRT, on écrirait quelque chose comme

isqrt(n) = isqrt2(n,0,1)
isqrt2(n,count,sum) =
  if sum<=n then isqrt2(n,count+1,sum + 2 * (count+1)+1) else count

On est ramené alors à la preuve d’un programme fonctionnel. Il s’agit là d’une instance de l’approche par plongement superficiel (shallow embedding en anglais) opposé à plongement profond (deep embedding), tel qu’expliqué dans le chapitre 2.

8.2.1  Le langage Why

C’est un langage fonctionnel auquel sont rajoutés quelques traits impératifs. Les types de base sont : int, bool, float et unit (habité par la constante void). Comme d’habitude avec les langages fonctionnels, il n’y a pas de distinction syntaxiques entre expressions et instructions : les instructions sont les expressions de type unit.

Le noyau fonctionnel est constitué des expressions suivantes :

Les traits impératifs sont introduits par

Remarque : pour simplifier on ne traite pas les définitions récursives ici, ni la levée et le rattrapage d’exception. Le langage complet est décrit dans le manuel utilisateur.

En Why, toute expression e peut être annotée, avec la notation des triplets de Hoare { pree { post }. Les boucles while doivent être annotée par

while e do {  invariant inv variant var } e done

pour spécifier un invariant de boucle, ainsi qu’un variant, une expression censée décroitre à chaque itération de la boucle, assurant ainsi la terminaison. Les annotations pre, post et inv sont des formules de logique du premier ordre, leur variables sont les variables du programme. De plus, dans les post on peut utiliser le mot-clé result pour référer à la valeur résultat de l’expression, et v@ pour désigner la valeur de v avant l’exécution de l’expression.

8.2.2  Typage avec effets

Comme un langage de programmation classique, le langage Why possède des règles de typage, et un programme doit être correctement typé pour que la génération des obligations de preuves puissent se faire. Comme ce langage est proche de Caml, le type en est assez proche aussi, mais on lui ajoute une spécificité qui est le typage des effets, qui consiste à préciser quelles sont les références qui sont lues et celles qui sont écrites.

Voici un exemple de programme très simple, qui va nous servir pour illustrer les mécanismes de Why :

  parameter montant : int ref

  let crediter = fun (s:int) -> 
    { s >= 0 }
    montant := !montant + s
    { montant = s + montant@ }

En tant que programme « Caml », on sait très bien inférer que crediter a le type int -> unit. Ce qu’on va faire en plus c’est de calculer ses effets, pour déterminer dans cet exemple que la référence montant est à la fois lue et écrite.

Un type avec effet est un triplet (type, variables lues, variables écrites). Voici un extrait des règles de typage de Why (cf [Fil03a] pour le reste).

 
x:t ∈ Γ     t  non ref
γ ⊢  x:(t,∅,∅)
        
x:t ref ∈ Γ
Γ ⊢  !x:(t,{x},∅)
  
 
 
Γ ⊢ e1:(t2 → (t1,R,W),R1,W1)     Γ ⊢  e2: (t2,R2,W2)     t2 non ref
Γ ⊢ (e1 e2):(t1,R1⋃ R2R,W1⋃ W2⋃ W)
 
 
 
Γ,x:t ⊢ e:(t′,R,W)
Γ ⊢ fun(x:t) → e:(t→ (t′,R,W),∅,∅)
 
 
 
x:t ref ∈ Γ     Γ ⊢ e : (t,R,W)
Γ ⊢ x:=e : (unit,{x}⋃ R,{x}⋃ W)
 

La règle de typage de l’application ci-dessus interdit d’appliquer une fonction à une référence. Une règle spéciale existe dans ce cas :

 
Γ ⊢ e1:(t2 ref → (t1,R,W),R1,W1)     Γ ⊢  r: (t2 ref,R2,W2)     r∉ (t1,R,W)
Γ ⊢  (e1 r):(t1[x ← r],R1⋃ R2⋃ R[x ← r],W1⋃ W2W[x ← r])
 
 

Il est fondamental de remarquer que cette règle interdit les alias, c.-à-d. de référencer la même chose avec deux noms différents. C’est une condition essentielle pour garantir la correction de la méthode Why. Voici un exemple typique :

  let incr2 = fun (x:int ref) (y:int ref) ->
    { true } begin x := !x + 1; y := !y + 1 end { x = x@ + 1 and y = y@ + 1 }

  parameter t : int ref

  let test = { true } (incr2 t t) { t = t@ + 1 }

Why signale une erreur de typage sur l’application (incr2 t t). Si c’était accepté, alors au vu de la post-condition de incr2, la post-condition t = t@ + 1 serait prouvable, or elle est fausse, c’est t=t@ + 2 qui est vrai.

Exercice 2   Dériver le jugement de typage
montant:int ref ⊢ crediter : (int→ (unit,{montant},{montant}),∅,∅))

On peut utiliser cette approche de typage avec effets pour définir des programmes Why de façon modulaire : un programme peut très faire appel à une autre fonction dont le code n’est pas donné, cette fonction doit seulement être spécifiée par son type avec effets, ainsi qu’avec un pré et une post-condition. Par exemple on peut écrire :

  parameter montant : int ref

  parameter crediter : s:int -> 
    { s >= 0 }
    unit reads montant writes montant
    { montant = s + montant@ }

  let test = fun (tt:unit) -> 
    { true }
    begin
      (crediter 50); (crediter 80)
    end
    { montant = montant@ + 130 }

8.2.3  Calcul de plus faible précondition

Avec l’inférence de type avec effets, on est capable d’associer à chaque sous-expression d’un programme un type avec effets. L’étape suivante consiste à leur associer aussi une pré et une post-condition : de deux choses l’une : soit l’expression considérée est déjà annotée (une boucle while, un identificateur de fonction, ou une expression explicitement annotée par l’utilisateur), soit on lui détermine une annotation par calcul de plus faible pré-condition, d’une manière très similaire à celui de la logique de Hoare classique, mais adaptée au langage Why.

Voici un extrait des formules de calcul de WP, les règles complètes sont dans le manuel de Why [Fil02] et dans [Fil99] .

WP(x,Q)=Q[result ← x
  WP(!x,Q)=Q[result ← x
  WP(x:=e,Q)=       WP(e,Q[result← ttx← resultx@← x]) 
  WP(e1;e2,Q)=WP(e1,WP(e2,Q)) 
  WP(if e1 then e2 else e3,Q)=       WP(e1,if result then WP(e2,Qelse WP(e3,Q
  WP(let x=e1 in e2,Q)=       WP(e1,WP(e2,Q)[x← result]) 

La règle pour l’application est l’une des plus complexe :

  WP((f e1 ⋯ en),Q) =  WP(e1,WP(e2,…,WP(en
 (Pf∧∀ w1,…,wkresultQfQ)[xn← result])…)[x1← result]) 

si f a le type avec effets annoté x1:t1xn:tn → {Pf} (t,R,W) {Qf}, et les expressions e1,…,en sont pures, c.-à-d. ne modifient aucune variable. Cette dernière condition fait qu’il peut arriver que l’outil Why peut parfois ne pas parvenir à générer les obligations de preuves, auquel cas il faut simplifier l’application concernée en introduisant des letin

Exercice 3   Annoter le code de crediter.

8.2.4  Traduction fonctionnelle

Il s’agit maintenant du cœur même de la méthode Why. Nous en donnons ici un aperçu, les détails étant dans[Fil99, Fil03a].

Le but est d’engendrer un programme fonctionnel Coq équivalent au programme Why complètement annoté. Ce programme comportera des « trous » pour les preuves des annotations logiques : les obligations de preuve. Celle-ci peuvent naturellement être prouvées dans Coq, pour obtenir alors un programme fonctionnel Coq certifié, équivalent au programme de départ, que l’on appelle la validation Why.

Interprétation fonctionnelle des types avec effets

Tout type avec effets annoté T={P} (t,vec(r),vec(w)) {Q} est interprété en un type Coq T :

∀ vec(x),P(vec(x)) → ∃ vec(y),∃ rQ(vec(x),vec(y),r)

La notation P(vec(x)) désigne la formule P où les occurrences des variables lues vec(r) sont substituées par les vec(x), et la notation Q(vec(x),vec(y),r) désigne la formule Q où, pour chaque variable v de vec(w), les occurrences de v sont remplacées par le y correspondant, les v@ par le x correspondant, pour chaque variable v de vec(r) qui n’est pas dans vec(w), chaque occurrence de v est remplacée par le x correspondant, et enfin result est remplacé par r. Il s’agit là d’exprimer le fait que les x désignent les anciennes valeurs des variables modifiables, alors que les y désignent les nouvelles valeurs.

En pratique, le ∃ est utilisé est celui dans Set, noté avec des accolades. Par exemple, le type avec effet de crediter :

s:int → {s >= 0} (unit,{montant},{montant}) { montant = s+montant@}),∅,∅)

est interprété par le type Coq

  forall (s: Z), forall (montant: Z), forall (H: s >= 0),
    { montant0: Z, result: unit | montant0 = s + montant }

Notons également que les types de base int, bool et float sont interprétés par leurs représentations mathématiques Coq (Z, bool et R) et donc en particulier les entiers ne sont pas bornés.

Interprétation fonctionnelle des programmes

On donne maintenant des règles de traduction d’une expression e de type avec effets T={P} (t,{r1,…,rk},{w1,…,wl}) {Q} dans un environnement Γ, en un terme Coq à trous e de type T dans l’environnement Γ obtenu en enlevant toutes les variables de type ref.

Remarques : les interprétations de l’application évaluent les arguments de l’application de droite à gauche. L’interprétation des boucles while [Fil99, Fil03a] utilise well_founded_induction tel qu’expliqué au chapitre 7.

Exemple 8   La validation à trous de crediter est
Definition crediter := 
  (fun (s: Z) (montant: Z) (Pre: s >= 0) =>
    let (result1, Post) :=
      exist (fun (result: Z) => result = (s + montant)) 
            (montant + s) (PO1 s montant Pre)
      (* : { result: Z | result = s + montant } *)
    in
      exist_2 (fun (montant1: Z) (result0: unit) => montant1 = s + montant) 
              result1 tt Post)
      (* : { result1: Z, result2:unit | result1 = s + montant } *)
PO1 (s:Z) (montant:Z) (Pre:s>=0) : montant + s = s + montant  
Proposition 3 (Correction [Fil99, Fil03a])   Pour toute expression e typée avec effets annotée, si les obligations de preuve de e sont prouvables, alors e vérifie sa spécification (c.à-d. que sa post-condition est valide quand sa pré-condition est satisfaite).

Pour la preuve de cette proposition, il faut définir formellement la sémantique de Why [Fil99, Fil03a].

8.3  Traitement des structures données complexes et application à d’autres langages de programmation

Why ne gère pas explicitement de structures de données complexes. Néanmoins, il a une approche modulaire, dans le sens où de même qu’il accepte des programmes en paramètre avec uniquement leurs spécifications, il accepte des types abstraits, et des prédicats et fonctions logiques abstraites sur ces types.

8.3.1  Exemple d’un programme avec un tableau : le drapeau hollandais

Il s’agit d’un exemple célèbre : un programme de tri linéaire quand il n’y a que trois valeurs (comme les couleurs du drapeau hollandais !) dû à Dijkstra [Dij76].

On introduit un type abstrait Why avec des axiomes :

parameter BLUE, WHITE, RED : color
logic iscolor : color -> prop
axiom color_elim : forall c:color. iscolor(c) -> c=BLUE or c=WHITE or c=RED

puis un premier programme Why uniquement spécifié, pour le test d’égalité des couleurs :

parameter eq_color : c1:color -> c2:color ->
  { } bool { if result then c1=c2 else c1<>c2 }

On introduit ensuite une axiomatisation des tableaux : on les représente en logique comme des tableaux « fonctionnels », c.-à-c. où la mise à jour d’une case de tableau retourne un nouveau tableau :

logic acc : colorarray, int -> color  (* acc(t,i) represente t[i] *)
logic length : colorarray -> int      (* longueur d'un tableau    *)
logic update : colorarray, int, color -> colorarray (* mise à jour t[i] := c *)
axiom length_pos: forall t:colorarray. 0 <= length(t)

axiom length_up: 
  forall t:colorarray. 
    forall i:int. forall v:color.
       length(update(t,i,v)) = length (t)

axiom acc_up_eq :
  forall t:colorarray. 
    forall i:int. forall v:color.
       acc(update(t,i,v),i) = v

axiom acc_up_neq :
  forall t:colorarray. 
    forall i:int. forall j:int. forall v:color.
       i <> j -> acc(update(t,i,v),j) = acc(t,j)

et on a les programme WHY suivant sur les tableaux :

parameter length_ : t:colorarray -> { } int { result = length(t) }

parameter acc_ : t:colorarray -> i:int -> 
  { 0 <= i < length(t) }
  color
  { result=acc(t,i) }

parameter update_ : t:colorarray ref -> i:int -> v:color -> 
  { 0 <= i < length(t) }
  unit reads t writes t
  { t = update(t@,i,v) }

noter les préconditions sur les bornes des tableaux utilisés.

On peut maintenant commencer par un petit programme qui echange deux éléments d’un tableau :

let swap = fun (t : colorarray ref) (i:int) (j:int) ->
  { 0 <= i < length(t) and 0 <= j < length(t) }
  let ti = (acc_ !t i) in
  let tj = (acc_ !t j) in
  begin
  (update_ t i tj);
  (update_ t j ti)
  end
  { length(t) = length(t@) and
    acc(t,i) = acc(t@,j) and 
    acc(t,j) = acc(t@,i) and
    forall k:int. i <> k and j <> k -> acc(t,k) = acc(t@,k) }

Pour écrire le programme de tri de Dijkstra, on introduit un predicat monochrome :

logic monochrome : colorarray, int, int, color -> prop

axiom mon1 : 
  forall t:colorarray. 
    forall i:int. forall j:int. forall c:color.
      monochrome(t,i,j,c) -> (forall k:int. i <= k < j -> acc(t,k)=c)
axiom mon2 : 
  forall t:colorarray. 
    forall i:int. forall j:int. forall c:color.
      (forall k:int. i <= k < j -> acc(t,k)=c) -> monochrome(t,i,j,c)

et le programme principal est alors

let flag = fun (t : colorarray ref) ->
  { forall k:int. 0 <= k < length(t) -> iscolor(acc(t,k)) }
  begin
  let b = ref 0 in
  let i = ref 0 in
  let r = ref (length_ !t) in
  while !i < !r do
   { invariant
       (forall k:int. 0 <= k < length(t) -> iscolor(acc(t,k)))
       and 0 <= b and b <= i and i <= r and r <= length(t)
       and monochrome(t, 0, b, BLUE)
       and monochrome(t, b, i, WHITE)
       and monochrome(t, r, length(t), RED)
     variant r - i }
    let c = (acc_ !t !i) in
    if (eq_color c BLUE)
    then
      begin (swap t !b !i); b := !b + 1; i := !i + 1 end
    else
     if (eq_color c WHITE)
     then i := !i + 1
     else
       begin r := !r - 1; (swap t !r !i) end
   done
  end
  { exists r:int. exists b:int.
           monochrome(t, 0, b, BLUE)
       and monochrome(t, b, r, WHITE)
       and monochrome(t, r, length(t), RED) }

Notons que les onze obligations de preuves engendrées pour ces deux programmes (swap et flag) sont prouvées entièrement automatiquement par Simplify.

8.3.2  Programmes Java et C

L’approche ci-dessus pour les tableaux simples peut être étendue à toute structure de données complexes, ce qui permet de traiter des « vrais » langages comme Java ou C : pour ceux-ci, la structure de la mémoire est modélisée avec les opérations logiques abstraites et des axiomes. L’outil Krakatoa [MPMU04] suit ce principe, et permet de traduire automatiquement un programme Java en un programme Why avec une telle modélisation. L’outil Caduceus, en cours de développement, fait de même avec les programmes C.

Remarquons aussi que cette approche pour modéliser les structures de données complexes peut être aussi utilisée pour traiter les entiers bornés : il suffit d’interpréter les opérations arithmétiques comme l’addition par une autre fonction logique. On a même le choix de permettre les débordements et faire des calculs modulo 232, ou bien imposer le non-débordement, en introduisant une fonction d’addition sur les entiers non bornés mais avec précondition de la forme

parameter bounded_add : x:int -> y:int ->
  { -2^31 <= x+y < 2^31 } int { result = x+y }

Previous Up Next