Licence CC BY-NC-SA

Preuve de programmes avec F* - Partie 1

Une première impression

Ça fait un petit bout de temps que les questions de preuve de programme m’intéressent. Ça viens en partie d’une certaine frustration que certaines propriétés ne se prêtent vraiment pas aux tests, comme vérifier qu’un parser ne crash pas, mais aussi du fait que je me retrouve en permanence à écrire du code pour vérifier que les arguments de ma fonction sont valide (par exemple que les pointeurs ne sont pas nuls). Même si je peux aller vérifier que maintenant ces vérifications ne sont pas nécessaires et que je peux mettre un commentaire pour dire que les arguments doivent être valide, forcément, il arrivera un jour où une petite modification de rien va casser les préconditions, ce qui ne sera pas forcément détecté par les tests.

Voici une liste non exhaustive de propriétés que l’on pourrais vouloir prouver:

  • on ne déréférence pas de pointeurs nuls.
  • le programme (ou certaines fonctions en particuliers) se finissent toujours.
  • on n’accède pas à un élément hors des limites d’un tableau.
  • on ne divise jamais un nombre par 0.
  • une fonction de recherche dichotomique n’est appelé qu’avec un conteneur dont le contenu est ordonné.
  • la fonction de comparaison donné à une fonction de tri possède certaines propriétés, comme la transitivité.
  • deux implémentations différente d’une fonction donnent le même même résultat pour toutes les entrées possibles.

Sur la papier, c’est génial parce que ça permet de garantir que certains bugs ou catégories de bugs ne sont pas présent dans un programme1. En contre partie, il va falloir prouver que toutes ces propriétés sont vrai. D’où la question: à quel point c’est galère de prouver des trucs non-triviaux? Question à laquelle je vais tenter de réponde (très subjectivement) dans cette série d’articles, en plus de présenter mes découvertes.

J’ai choisi de me focaliser sur le langage F* pour plusieurs raisons:

  1. il est associé à un SMT solver (Z3), qui est sensé s’occuper des parties "triviales" des preuves. C’est absolument nécessaire pour moi: j’ai essayé d’utiliser Lean (qui n’a pas de SMT solver) avant et après avoir passé plusieurs heures à essayer de prouver que 1 > 0, sans réussir, j’ai jeté l’éponge.
  2. c’est avant tout un langage de programmation, avant d’être un outil de preuve de programme. Donc je m’attends à pouvoir écrire un programme utile à peu près aussi facilement que dans n’importe quel autre langage de programmation.
  3. il m’a donné l’impression d’être l’un des projets les plus mature dans le domaine satisfaisant les deux contraintes précédentes.

Je suis encore un gros débutant avec F* et dans la preuve de programmes de manière générale. Il est parfaitement possible que je raconte des grosses bêtises à un moment dans ce billet, si ce n’est pas déjà fait. Prenez ce que je dis avec des pincettes.

Le logo de l’article est celui de F*, distribué sous licence Apache 2.0.

  1. À supposer que l’outil de preuve utilisé n’a pas lui-même des bugs et que les propriétés que l’on veut garantir sont correctement décrites. ^^↩

Une introduction rapide

De prime abord, F* est un langage fonctionnel et ressemble beaucoup à OCaml, dont il s’est inspiré. Ça fait un bout de temps que je n’ai pas touché à OCaml, mais j’ai pu noter deux différences assez importantes.

Premièrement, F* n’a ni variables mutables, ni boucles. Ça n’est pas exactement dérangeant étant donné que ce sont des fonctionnalités qui peuvent facilement rendre les choses plus difficiles à prouver et que l’on peut facilement s’en passer à coup de récursion. Il est cependant possible d’imiter ces fonctionnalités (et plus) en utilisant des monades, ce qui ressemble plus à du Haskell qu’à du OCaml.

Deuxièmement, F* à un système de type qui laisse beaucoup plus de libertés qu’en OCaml:

  • On peut appliquer des restrictions arbitraires aux types. Par exemple, les entiers strictement positifs s’écrivent i:int{i > 0}, à lire "les i de type int qui satisfont i > 0". Ça peut être utilisé pour des trucs nettement plus fantaisistes, comme pour définir un type qui contient les nombres premiers avec quelque chose du genre p:int{isPrime p}.
  • Le type d’un argument ou de la valeur de retour d’une fonction peut dépendre des arguments précédents. Donc a:int -> b:int{b > a} -> c:int, c’est simplement une fonction dont le premier argument est un entier, le deuxième argument est un entier strictement supérieur au premier argument et dont la valeur de retour est un entier1.
  • On peut avoir un type en tant qu’argument ou valeur de retour d’une fonction. Donc écrire une fonction qui prend en argument un entier n et qui retourne le type correspondant aux vecteurs de booléens de taille n, c’est pas un soucis.

C’est en utilisant cette liberté dans la définition des types que l’on va pouvoir introduire toutes les propriétés que l’on veut prouver. Par exemple, le type de la fonction valeur absolue peut s’écrire: a:int -> b:int{b >= 0 && (b = a || b = -a)}. C’est à dire que l’on prend en entrée un entier a et qu’en sortie on a un entier positif b qui est égal à l’entrée ou à l’opposé de l’entrée. Dans cet exemple, le type de sortie contraint entièrement la fonction et pour chaque entrée, une seule valeur de sortie est possible. Dans des cas un peu plus complexes, ça peu devenir trop long ou compliqué de contraindre autant le type de sortie, donc on se contentera du stricte minimum pour pouvoir prouver les propriétés qui nous intéressent vraiment.

  1. c’est pas exactement vrai parce que les fonctions sont curryfiées. Mais bon, ça n’a pas une grande importance ici.↩

Un objectif non-trivial pour tester F*

Afin de me donner une bonne impression sur les capacités de F* et de ses limitations, je me suis donné pour objectif d’écrire deux implémentations différentes d’une fonction qui résout un problème simple (mais pas trop) et d’ensuite prouver que ces deux fonctions sont équivalentes.

Le problème

Il est très fortement inspiré du problème numéro 1 du projet Euler: étant donné 3 entiers positifs aa, bb et cc, calculez la somme des entiers positifs multiple de aa ou bb strictement inférieurs à cc.

Solution 1

L’idée de la première implémentation est très simple: prendre tous les entiers positifs strictement inférieurs à cc, les filtrer pour ne conserver que les entiers multiples de aa ou bb et en faire leur somme.

Solution 2

Le résultat peut se calculer via une formule qui se trouve sans trop de difficultés en manipulant notre somme. Prenons a=2a=2, b=3b=3 et c=13c=13.

Les entiers qui sont multiples de 22 ou 33 et strictement inférieurs à 1313 sont: 22, 33, 44, 66, 88, 99, 1010 et 1212.

On peut réécrire la somme comme ceci:

2+3+4+6+8+9+10+12=(2+4+6+8+10+12)+(3+6+9+12)−(6+12)=2×(1+2+3+4+5+6)+3×(1+2+3+4)−6×(1+2)\begin{aligned} 2+3+4+6+8+9+10+12 &= (2+4+6+8+10+12)+(3+6+9+12)-(6+12) \\ &= 2\times(1+2+3+4+5+6)+3\times(1+2+3+4)-6\times(1+2) \\ \end{aligned}

On se retrouve avec 3 cas de "somme des entiers positifs de 1 à nn", dont la formule est: n×(n+1)2\frac{n\times(n+1)}{2}

On serait donc tenté de généraliser la somme en:

aA×(A+1)2+bB×(B+1)2−a×bAB×(AB+1)2a\frac{A\times(A+1)}{2}+b\frac{B\times(B+1)}{2}-a\times b\frac{AB\times(AB+1)}{2}

Avec A=⌊ca⌋,B=⌊cb⌋et AB=⌊ca×b⌋A = \left\lfloor\frac{c}{a}\right\rfloor, B = \left\lfloor\frac{c}{b}\right\rfloor \text{et } AB = \left\lfloor\frac{c}{a\times b}\right\rfloor

Cependant, les nombres en commun dans les deux premières somme et qui doivent être retiré avec la troisième somme ne correspondent aux multiples de a×ba\times b que si aa et bb sont premiers entre eux. S’ils ne le sont pas, les nombres en commun dans les deux premières sommes sont les multiples du plus petit commun multiple de aa et bb, qui est a×ba\times b s’ils sont premiers entre eux. Donc la bonne formule est:

aA×(A+1)2+bB×(B+1)2−ppcm(a,b)AB×(AB+1)2a\frac{A\times(A+1)}{2}+b\frac{B\times(B+1)}{2}-ppcm(a, b)\frac{AB\times(AB+1)}{2}

Avec A=⌊ca⌋,B=⌊cb⌋et AB=⌊cppcm(a,b)⌋A = \left\lfloor\frac{c}{a}\right\rfloor, B = \left\lfloor\frac{c}{b}\right\rfloor \text{et } AB = \left\lfloor\frac{c}{ppcm(a, b)}\right\rfloor

Implémentation de la solution 1

Sans plus attendre, on va se pencher sur l’implémentation de la première solution.

Afin de faire un peu plus qu’appeler 3 fonctions standard (ce qui ne serait pas très intéressant), j’ai décider de ré-implémenter un type pour la liste d’entiers, ainsi que les quelques fonctions associés qu’il faudra.

Représenter une liste d’entiers

Toujours pour pimenter un peu les choses et tester les possibilités de F*, j’ai défini un type vec qui utilise le type de ses éléments (normal), mais aussi le nombre d’éléments qu’il contient. Donc vec int 3 correspond à une liste de 3 entiers.

Comme pour toute bonne liste dans un langage fonctionnel, on a une liste vide Nil et un constructeur Cons qui prends un élément (la tête, hd) et le reste de la liste (la queue, tl):

type vec a : nat -> Type =
  | Nil : vec a 0
  | Cons : #n:nat -> hd:a -> tl:vec a n -> vec a (n+1)

Dans F*, : permet d’indiquer le type d’un truc. Donc Cons : blabla dit que Cons à le type blabla. C’est utilisé aussi au sein du type de Cons, dans hd:a qui dit que hd est de type a (qui est le type des éléments de la liste). Ici, les noms hd et tl pourraient être omis, mais je les ai laissé pour indiquer à quoi correspondent chaque élément.

Le type nat correspond aux entiers naturels (donc i:int{i >= 0}), ce qui nous permet de garantir qu’on n’aura pas de liste avec un nombre négatif d’éléments. On voit au passage l’avantage d’avoir un SMT solver: sans rien dire de plus, le compilateur va être capable de vérifier qu’avec n un entier naturel, n+1 est aussi un entier naturel.

L’argument #n:nat est un argument implicite (indiqué par le #), que F* devra déduire. Par exemple, dans Cons 2 Nil, Nil est de type vec int 0, donc F* déduit que le n vaut 0.

Voici quelques exemples de listes pour bien comprendre comment ça fonctionne:

// Une liste d'entiers vide.
let empty : vec int 0 = Nil

// Une liste qui contient un seul entier (42).
// J'ai réutilisé `empty` déclaré plus haut, mais j'aurais pu utiliser Nil.
let one_element : vec int 1 = Cons 42 empty

// Une liste de 3 booléens.
let many_bools : vec bool 3 = Cons true (Cons false (Cons true Nil))

Sommer des entiers

On continue sur du simple en définissant la fonction qui va nous servir à sommer une liste d’entiers:

let rec sum (#n:nat) (v:vec nat n) : nat
  = match v with
    | Nil -> 0
    | Cons hd tl -> hd + sum tl

Encore une fois, on retrouve un argument implicite pour n. Et encore une fois, j’apprécie de ne pas avoir à écrire moi-même une preuve du fait que la fonction se termine, que 0 est un entier naturel et que le résultat de notre somme d’entiers naturels est effectivement un entier naturel.

Ça peut paraître con dit comme ça, mais je rappelle avoir été traumatisé par Lean, où je n’ai pas été capable de prouver que 1 > 0 après plusieurs heures à essayer. J’espère que ça remet en perspective à quel point, même un truc qui paraît simple, peut être difficile à prouver quand on ne sait pas comment faire.

Générer une liste d’entiers successifs

Même si on a uniquement besoin d’une liste d’entiers de 1 à N, j’ai généralisé la fonction pour qu’elle donne une liste d’entiers entre a et b (inclus) avec a <= b.

let rec generate (a:nat) (b:nat{b >= a})
  : Tot (vec nat (b-a+1)) (decreases (b-a))
  = if a = b then
      Cons a Nil
    else
      Cons a (generate (a+1) b)

Ici, on a 2 cas de types dépendants: le type de b, qui dépend de a et le type de retour qui dépend de a et b pour indiquer la taille de la liste de retour.

Le type de retour n’est pas simplement vec nat (b-a+1), parce que F* n’est pas capable de prouver tout seul que la fonction se termine. En revanche, il suffit de lui donner une valeur entière positive, dépendante des arguments de la fonction et strictement décroissante lors des appels récursifs et il sera capable de faire le reste de la démonstration pour prouver que la fonction se termine1.

Tot (vec nat (b-a+1)) (decreases (b-a)) indique que la fonction est totale (c’est à dire qui n’a pas d’effets de bords et qui se termine), retourne un vec nat (b-a+1) et que b-a décroît strictement lors des appels récursifs.

Filtrer une liste

On est maintenant sur la partie de l’implémentation qui m’a posé le plus de problèmes. On veut une fonction qui prend en argument une fonction de filtre de type a->bool, une liste de type vec a n et qui retourne une liste de type vec a m. Du moins, c’est ce que j’ai initialement essayé, mais le compilateur a dit non.

Le problème devient apparent en se penchant sur l’implémentation, qui contient cette condition:

if f hd then
  // Si l'élément passe le filtre, on doit l'ajouter au reste de la liste filtré
  Cons hd (filter f tl)
else
  // Sinon, la liste de retour est le reste de la liste filtré
  filter f tl

Donc si filter f tl est de type vec a m, alors Cons hd (filter f tl) est de type vec a (m+1) et les deux branches de notre condition ont des types différents, ce que le compilateur n’apprécie pas du tout.

Catastrophe! Tonnerre de Brest! Nom d’une pipe! Sacrebleu! Mais comment résoudre ce problème? Est-ce que je me suis tiré une balle dans le pied en utilisant un type de liste dont la taille fait partie du type?

Et bien non, la taille de la liste de retour est exactement le nombre d’éléments qui sont acceptés par le filtre. Littéralement. Écrivons-donc cette fonction:

let rec num_filtered #a (#n:nat) (f:a -> bool) (v:vec a n) : (r:nat{r <= n})
  = match v with
    | Nil -> 0
    | Cons hd tl -> (if f hd then 1 else 0) + num_filtered f tl

J’y ai ajouté une petite touche sur le type de retour pour indiquer que le nombre d’éléments qui passent le filtre est inférieur ou égal au nombre d’éléments de la liste d’entrée. C’est pas super utile, mais vu que F* est capable de nous prouver ça tout seul (enfin, avec l’aide de Z3), ça coûte pas grand chose.

Muni de cette fonction, on peut donc dire que le type de retour de notre fonction filtre est vec a (num_filtered f v), qui dépend donc des deux arguments de la fonction:

let rec filter #a (#n:nat) (f:a -> bool) (v:vec a n) : vec a (num_filtered f v)
  = match v with
    | Nil -> Nil
    | Cons hd tl ->
      if f hd then
        Cons hd (filter f tl)
      else
        filter f tl

Le cerise sur le gâteau, c’est qu’il n’est pas nécessaire de donner plus d’info pour que F* soit capable de prouver que le type de retour est correcte et que la fonction se termine. Elle est pas belle la vie?

On met tout ensemble

Voilà, toutes les fonctions utilitaires nécessaires pour la première solution sont défini. Sans plus attendre, voici la solution:

let answer1 (a:pos) (b:pos) (c:nat) : nat
  = let candidates = generate 0 c in
    let ab_filter = filter (fun (x:nat) -> x%a = 0 || x%b = 0) in
    sum (ab_filter candidates)

La dernière chose à noter, c’est que a et b sont défini comme pos, c’est à dire i:int{i > 0} parce que la division et le modulo entier ne sont défini que sur les entiers non-nuls.

Et voilà. Au final, il n’y a quasiment rien eu à faire pour que F* soit capable de vérifier une bonne quantité de propriétés, notamment de terminaison, mais aussi certaines propriétés arithmétiques. Jusque là, c’est très prometteur.

  1. C’est suffisant, mais pas nécessaire. F* accepte en fait n’importe quel mesure, qui est une valeur dépendant des arguments de la fonction, qui décroît strictement lors des appels récursifs et défini sur un ensemble qui n’admet pas de chaîne infiniment décroissante. Il n’est d’ailleurs pas nécessaire que l’ordre soit total sur l’ensemble.↩

Pour rendre le billet plus digeste et plus facile à écrire, j’ai décidé de le découper en 3 (j’espère) parties.

Je parlerais de l’implémentation de la deuxième solution dans un second billet, où je vais devoir mettre les mains dans le cambouis parce qu’on arrive très vite sur des propriétés arithmétiques non-triviales, comme prouver que l’algorithme d’Euclide pour calculer le PGCD est correcte.

La preuve final que les deux solutions donnent le même résultat fera probablement l’objet d’un troisième billet. À moins que le troisième billet explique pourquoi je n’y arrive pas. :D

Petit teaser pour la suite, voici comment on peut prouver qu’avoir un élément x dans la liste generate a b est équivalent à a <= x && x <= b:

// Fonction indiquant si une valeur x est dans le vecteur v.
// eqtype contient tous les types sur lesquels l'égalité est défini,
// on peut donc appeler la fonction `=` sur les éléments de a.
let rec contains (#a:eqtype) (#n:nat) (x:a) (v:vec a n) : bool
  = match v with
    | Nil -> false
    | Cons hd tl -> if hd = x then true else contains x tl

// La preuve est récursive.
let rec generate_contains (x:nat) (a:nat) (b:nat{b >= a})
  // ensures indique la propriété que l'on veut prouver.
  : Lemma (ensures contains x (generate a b) <==> a <= x && x <= b)
          (decreases (b-a)) // Ça, c'est pour montrer la terminaison de la preuve
  = if a = b then
      () // Cas trivial, (generate a b) n'a qu'un seul élément
    else if a = x then
      () // Cas trivial, x est le premier élément de (generate a b)
    else
      // Cas récursif, x est dans (generate (a+1) b)
      generate_contains x (a+1) b

Comme vous pouvez le voir, F* se débrouille très bien pour gérer les cas triviaux, mais aussi pour gérer tous les détails que je n’ai pas écris, mais qui sont nécessaire pour l’application du cas récursif.

13 commentaires

L’exemple est sympa pour tester effectivement.

Question : pourquoi avoir éjecté Why3 de la liste ? Il me semble qu’il répond aux contraintes que tu t’es fixé. Les différences pour moi:

  • Why3 extrait en sortie vers du Ocaml pour produire le code exécutable,
  • Ce ne sont pas des types dépendants mais plutôt des contrats + invariants de type parfois,
  • On a accès à plein de prouveurs automatiques et interactifs pour terminer les preuves.

Par exemple le code que tu mets tout en bas avec Why3, tout prouvé automatiquement aussi:

module M
  use list.List
  use list.Mem
(* but we could write it:
  predicate mem (x: 'a) (l: list 'a) = match l with
    | Nil      -> false
    | Cons y r -> x = y \/ mem x r
    end
*)
  use int.Int

  let rec function generate (a b:int) : list int
    requires { 0 <= a /\ a <= b }
    variant  { b - a }
    =
    if a = b then
      Cons a Nil
    else
      Cons a (generate (a+1) b)

  let rec lemma generate_contains (x a b: int)
    requires { 0 <= x /\ 0 <= a /\ a <= b }
    ensures  { Mem.mem x (generate a b) <-> a <= x /\ x <= b }
    variant  { b - a }
  =
    if a = b then ()
    else if a = x then ()
    else generate_contains x (a+1) b
end
+0 -0

En essayant de trouver un outil qui corresponde au mieux à ce que je cherche, je me suis retrouvé à regarder facilement 10–20 projets différents et j’ai fait le tri probablement trop rapidement.

De mémoire, j’ai du regarder l'introduction et ça m’a donné l’impression que ça ne correspondait pas à ce que je cherchais pour plusieurs raisons:

  • le seul exemple de cette page est un truc à prouver, et dans la page suivante, le premier exemple ne contient lui aussi pas de code. Donc sans regarder plus loin, ça donne l’impression que ce n’est pas fait pour écrire du code.
  • il y a tout plein de captures d’écran d’une GUI, ce qui laisse penser (probablement à tort) que la CLI n’est pas géniale, alors que je préfère largement utiliser vim + cli pour du dev.
  • Why3 n’a pas de page Wikipedia et ne fait pas partie cette comparaison. Pour un projet qui a plus de 10 ans, ça donne pas la meilleur des impressions.

C’est clairement pas des arguments super solide, mais sachant que j’avais regardé F* avant et qu’il semblait correspondre à mes critères, je n’ai pas été regarder plus loin.

Au passage, F* génère aussi du code OCaml, donc ce n’est pas une différence avec Why3.

Sur les autres différence, la possibilité d’utiliser différents prouveurs automatiques et interactif semble être un bon point en supposant qu’ils ont chacun leurs domaines où ils sont plus efficaces que les autres.

Pour la différence entre types dépendants vs contrats+invariants, est-ce qu’il y a une différence fondamentale entre les deux? À première vue, j’ai l’impression que non, mais je rate peut-être quelque chose.

+0 -0

le seul exemple de cette page est un truc à prouver, et dans la page suivante, le premier exemple ne contient lui aussi pas de code. Donc sans regarder plus loin, ça donne l’impression que ce n’est pas fait pour écrire du code.

Pour le coup, on peut. Il a surtout été pensé pour être un labo à prouver des algorithmes (bien plus que de propriétés). Dans mon labo, on a commencé à s’en servir pour réécrire un bout de Frama-C par exemple.

D’ailleurs, autre point que j’avais oublié dans la comparaison, c’est que Why3 inclut un fragment impératif et les constructions qu’il faut pour faire de la preuve dessus.

il y a tout plein de captures d’écran d’une GUI, ce qui laisse penser (probablement à tort) que la CLI n’est pas géniale, alors que je préfère largement utiliser vim + cli pour du dev.

La GUI n’est pas géniale effectivement (même si franchement, elle a énormément progressé), mais de toute façon, elle ne sert que pour les toutes dernières étapes de preuve. Donc de toute façon, tu aurais utilisé ton éditeur. Un point c’est qu’elle peut servir à faire certaines transformations quand les SMT solvers galèrent et qu’ils ont besoin d’un coup de main. Ça peut aider à finir les preuves.

Why3 n’a pas de page Wikipedia et ne fait pas partie cette comparaison. Pour un projet qui a plus de 10 ans, ça donne pas la meilleur des impressions.

Je suis assez convaincu qu’il doit en manquer d’autres. Il n’y a pas tant de contributeurs pour cette page, et c’est facile de louper des travaux, même importants, du domaine. Après, je suis d’accord qu’il n’a pas le même rayonnement que F* (et pas le même support financier non plus).

Au passage, F* génère aussi du code OCaml, donc ce n’est pas une différence avec Why3.

J’avais en tête que c’était du C, via leur compilo Kremlin, mais c’est vrai que c’était dans un cas particulier d’extraction.

Sur les autres différence, la possibilité d’utiliser différents prouveurs automatiques et interactif semble être un bon point en supposant qu’ils ont chacun leurs domaines où ils sont plus efficaces que les autres.

C’est le cas. Why3 est le backend qu’on utilise pour Frama-C/WP, et c’est aussi celui utilisé par Ada/Spark. Et ce qu’on constate sur des grosses études de cas c’est qu’il n’y a aucun prouveur automatique qui arrive à tacler toutes les preuves de manière automatique. Ça peut commencer à se voir quand tu as quelques dizaines d’obligations de preuve, c’est hyper clair quand tu vas taper dans les centaines de milliers d’objectifs générés (typiquement sur du logiciel industriel). Combiner les solveurs maximise ce que tu vas pouvoir vérifier automatiquement.

Il va s’ajouter à ça que tous les prouveurs ne proposent pas les mêmes fonctionnalités (et encore moins aussi efficace une nouvelle fois). Par exemple, j’utilise régulièrement CVC4 pour demander un éventuel contre-exemple quand certaines preuves échouent.

Pour la différence entre types dépendants vs contrats+invariants, est-ce qu’il y a une différence fondamentale entre les deux? À première vue, j’ai l’impression que non, mais je rate peut-être quelque chose.

Sur le plan fondamental, pas vraiment non.

Par contre, écrire des spécifications, ça peut vite devenir chronophage, et représenter beaucoup de lignes de code quand on veut prouver des propriétés un peu compliquées. À l’usage, encoder ça dans des types peut devenir un peu pénible à la relecture, ou même quand tu dois triturer un peu les formulations pour que les solveurs automatiques soient contents.

Après sur ce point, ça tient plus de l’avis personnel.

+0 -0

Une raison de ne pas avoir Why3 dans la page Wikipédia des assistants de preuve, c’est que ce n’est pas vraiment un assistant de preuve (comprendre: aide à la preuve d’énoncés mathématiques), il faut lui tordre le bras pour faire des preuves sur des énoncés mathématiques compliqués. Dans une certaine mesure c’est le cas aussi de F (ou Idris), mais il y a moins besoin de les tordre car leur logique est clairement assez expressive pour dire tout ce dont on pourrait avoir envie, ce sont surtout les méthodes de preuve manuelles qui sont un peu pénibles (car F investit plus sur la preuve automatique, et Idris sur les aspects programmation).

Sur le reste des retours de @Berdes: c’est intéressant et je pense que ce serait utile à faire remonter aux gens de Why3. Pour l’aspect "j’ai lu l’intro et…", c’est aussi un peu un coup de "pas de chance", parce que le site web de Why3 a la description suivante qui me semble claire:

Why3 is a platform for deductive program verification. It provides a rich language for specification and programming, called WhyML, and relies on external theorem provers, both automated and interactive, to discharge verification conditions. (See the list of supported provers below.) Why3 comes with a standard library of logical theories (integer and real arithmetic, Boolean operations, sets and maps, etc.) and basic programming data structures (arrays, queues, hash tables, etc.)

Ceci dit, je suis d’accord avec la critique, dans le fond, que Why3 n’est pas assez utilisé pour écrire de vrais programmes, je pense que c’est un angle mort de la communauté et qu’ils n’ont pas fait assez d’effort pour avoir autre chose à dire que "… mais on peut extraire et lier avec du OCaml". J’aimerais bien, par exemple, avoir un dépôt git d’exemple quelque part, bien mis en avant dans la documentation, qui contient le code d’un petit programme dont le coeur de métier est prouvé correct par Why3 (par exemple: une petite calculatrice en ligne de commande), avec la logique OCaml autour pour le "faire tourner" et le système de build (intégration à Dune ou compagnie), etc.

+0 -0

Sur le reste des retours de @Berdes: c’est intéressant et je pense que ce serait utile à faire remonter aux gens de Why3.

C’est pas faute de les tanner régulièrement pour avoir plus de doc et de pub autour de la plateforme :-°

En vrai, du côté de l’équipe Frama-C, on pourrait aussi contribuer à la doc etc. Mais on leur jette pas du tout la pierre, chez nous aussi on a du mal à le faire parce que ça prend beaucoup de temps :(

+0 -0

Je ne sais pas sous quelle forme tu les tannes, mais je trouve que pointer du doigt des petits changements concrets qui ont concrètement posé problème à quelqu’un peut être plus motivant, du point de vue de la personne qui reçoit le feedback, qu’une exhortation d’ensemble à une tâche quasi-impossible (écrire de la bonne documentation, faire de la pub).

(J’ai écrit à why3-club, tu as peut-être vu passer.)

+0 -0

Je ne sais pas sous quelle forme tu les tannes, mais je trouve que pointer du doigt des petits changements concrets qui ont concrètement posé problème à quelqu’un peut être plus motivant, du point de vue de la personne qui reçoit le feedback, qu’une exhortation d’ensemble à une tâche quasi-impossible (écrire de la bonne documentation, faire de la pub).

gasche

C’est généralement quand on discute d’un truc qu’on est en train de faire, et au détour de la discussion. C’est jamais vraiment posé "formellement". Comme je disais, je leur jette vraiment pas la pierre à ce sujet. On aimerait tous que notre outil soit mieux documenter, mieux mis en avant, mieux …

+0 -0

Merci pour ce billet !

deux implémentations différente d’une fonction donnent le même même résultat pour toutes les entrées possibles.

Oh là ! D’après le théorème de Rice ce sont des choses indécidables non ?

Ici c’est rendu possible car on contraint beaucoup l’entrée ?

+0 -0

Merci pour ce billet !

deux implémentations différente d’une fonction donnent le même même résultat pour toutes les entrées possibles.

Oh là ! D’après le théorème de Rice ce sont des choses indécidables non ?

ache

Non, tout comme avec le problème de l’arrêt, l’indécidabilité dans le théorème de Rice viens du fait que c’est indécidable pour certains programmes. Autrement dit, il est possible de construire un programme pour lequel il est impossible de prouver s’il fini ou non. Par contre, pour un programme utile quelconque les chances pour que ce soit indécidable sont approximativement 0.

+1 -0

Ce que dit le théorème de Rice, c’est qu’une analyse statique, automatique, exacte et sound (pas trouvé de traduction) capable de démontrer une propriété non triviale qui dépend de la sémantique d’un programme n’existe pas. Mais si tu te débarrasses d’une partie des contraintes, ça peut devenir décidable.

Par exemple ici, la méthode n’est pas complètement automatique : on annote les types avec des propriétés particulières qui guident le processus de preuve. Et selon la propriété à prouver ou la complexité du programme, on peut devoir ajouter beaucoup d’information de ce genre.

(En test, on supprime la soundness et le côté statique, et on a une méthode exacte et automatique. En interprétation abstraite, on supprime l’exactitude, et on a une méthode statique; *sound et automatique. Et on peut trouver d’autres méthodes qui suppriment d’autres contraintes).

+1 -0

Il me semble que soundness correspond à la notion de correction (pour une analayse: si elle dit oui, alors le programme est vraiment correct), complémentaire de la notion de complétude (si le programme est vraiment correct, alors elle dit oui). Décider une propriété c’est dire "oui" exactement quand elle est vraie, et "non" exactement quand elle est fausse. En pratique les analyses statiques automatiques de propriétés indécidables sont en général conçues pour être correctes mais pas complètes, mais il y en a qui sont complètes et pas correctes et quelques trucs mal fichus qui ne sont ni l’un ni l’autre "parce que c’est plus facile de pouvoir parfois dire n’imp' à l’utilisateur".

+2 -0

Pour traduire soundness, je préfère utiliser le terme sûreté, que je trouve moins connoté : quand on dit d’une analyse unsound qu’elle est incorrecte, ça peut sous-entendre qu’elle est buguée ou mal conçue, ce qui n’est pas forcément le cas. En revanche, elle n’est pas sûre parce qu’on risque de se planter si on fait confiance à son résultat pour supposer l’absence d’erreurs dans le programme cible.

En pratique les analyses statiques automatiques de propriétés indécidables sont en général conçues pour être correctes mais pas complètes, mais il y en a qui sont complètes et pas correctes et quelques trucs mal fichus qui ne sont ni l’un ni l’autre "parce que c’est plus facile de pouvoir parfois dire n’imp' à l’utilisateur".

Historiquement, la recherche en analyse statique automatique s’est souvent concentré sur l’objectif « certification de programmes ». Il est alors indispensable d’avoir des analyses sûres : il est impossible de garantir qu’un programme est correct, ou plus précisément qu’il est exempt d’une certaine classe d’erreurs, si l’analyse en elle-même peut ignorer certaines de ces erreurs.

Mais il existe aussi une autre application de l’analyse statique qui a plutôt envie d’avoir des analyses complètes, c’est la recherche de bugs. Un peu par provocation, on dit alors parfois que ça ne sert à rien de me montrer tout un tas de bugs qui n’existent pas dans mon programme alors que je n’ai même pas fini de corriger ceux qui existent. La complétude est alors utile parce qu’elle aide les développeurs à produire du travail « utile », à savoir corriger des vrais bugs plutôt que passer du temps à réaliser que l’analyse n’était pas assez précise.

Dans le cas des analyses complètes, on doit alors accepter de perdre la sûreté, mais on considère que ce n’est pas forcément très grave : tant qu’il reste des bugs à corriger et que l’analyse me les montre, peu importe qu’elle me les montre tous, de toute façon j’ai du pain sur la planche. Et quand elle ne me montrera plus rien, alors il sera temps de me poser la question de la sûreté pour éventuellement certifier que j’ai bien tout corrigé.

Les analyses « mal fichues qui font n’imp » se retrouvent souvent dans une de ces deux catégories : soit c’est des analyses qui cherchent à prouver des choses, auquel cas c’est un vrai problème parce qu’on ne peut pas leur faire confiance, soit elles veulent trouver des choses, auquel cas c’est quand même beaucoup moins grave. Le risque est de faire travailler un développeur pour rien vs. faire décoller une fusée qui risque d’exploser, ce n’est pas du tout symétrique. Du coup, comme effectivement il est souvent beaucoup plus facile d’écrire une analyse qui peut parfois « dire n’imp » à l’utilisateur, il est en pratique assez fréquent que les outils de recherche de bug ne soient en réalité pas vraiment complets. C’est un peu vexant d’un point de vue théorique, et scientifiquement je ne suis pas sûr que ce soit un sujet de recherche très intéressant, mais on peut quand même faire des choses très utiles avec.

Infer et Polyspace Bug finder sont des exemples d’analyses « qui veulent trouver des bugs, qui ne sont pas sound parce que ça ne serait pas utile, qui aimeraient bien être complètes mais comme c’est trop dur ne le sont pas tout-à-fait ». Ça reste d’excellents outils qui ont largement fait leurs preuves, et surtout des beaux exemples d’application de la recherche en analyse statique (les deux sont basés sur l’interprétation abstraite) à l’échelle de (très) gros projets industriels.

(Remarque : la suite Polyspace a aussi un outil sûr, Code prover, basé aussi sur l’interprétation abstraite mais qui sert à certifier du code.)

+1 -0
Connectez-vous pour pouvoir poster un message.
Connexion

Pas encore membre ?

Créez un compte en une minute pour profiter pleinement de toutes les fonctionnalités de Zeste de Savoir. Ici, tout est gratuit et sans publicité.
Créer un compte