Spécification et preuve formelle [Résolu]

[hellfoust]

Bonjour,

N'y connaissant pas grand chose en preuve formelle, je cherche à m'exercer sur un exemple (un petit programme style résolution de sudoku). J'avais essayé OCaml et Haskell il y a 3 ans mais je ne me souviens plus très bien de la syntaxe.

Donc j'aimerais avoir votre avis sur le langage le plus adapté pour transformer une spécification algébrique en programme (et inversement , un programme en spéc), puis de faire la preuve de la spéc (avec un arbre de preuve, en utilisant les axiomes, la réflexion, la symétrie, la transitivité, la congruence, ...).

Ca ne dépend pas du langage, mais j'aimerais aussi utiliser un peu des outils d'aide à la preuve, qui font pour nous les étapes les plus faciles comme la symétrie ou la transitivité.

Pour info, voici la spécification algébrique des entiers naturels et de l'addition :

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
Sortes :
  Nat

Constructeurs :
  0 : -> Nat
  plusUn : Nat -> Nat

Fonctions :
  plus : Nat * Nat -> Nat

Axiomes :
  plus(x, 0) = x
  plus(x, plusUn(y)) = plus(plusUn(x), y)

Variables :
  x : Nat
  y : Nat

Je vous remercie pour votre aide.

[gasche]

Il y a plusieurs degrés de formalisme possible. Il faut t'attendre à ce que plus c'est formel, plus c'est lourd et plus il faut travailler pour faire la preuve. Les outils de preuve formelle mécanisée (vérifiée par ordinateur) ne sont pas encore aussi pratiques à utiliser qu'ils le pourraient, donc faire une preuve formelle complète c'est un travail très conséquent.


L'outil le plus populaire dans le coin est Coq.
C'est un outil basé sur l'idée qu'un système de typage suffisamment puissant peut aussi devenir un système de preuve. Tu peux donc écrire des preuves et des programmes dans un même langage (mais est donc très contraignant pour la programmation), et il y a aussi un langage spécialisé pour écrire des preuves "automatisées", c'est à dire en fait écrire un petit programme qui trouve tout seul la preuve, au lieu de construire directement l'arbre de preuve toi-même.
Il est très populaire en France parce que développé sur place (cocorico), mais ça reste un des outils les plus reconnus dans le domaine (avec Isabelle) à l'international. En particulier, si tu demandes de l'aide sur ce forum, ça devrait aller.

Comme je l'ai dit, écrire des preuves avec Coq reste assez lourd. Essaie et tu verras, en particulier au début on ne connaît pas les outils et c'est l'enfer; ensuite on se familiarise avec l'outil et ça va un peu mieux, mais ça reste du lourd (écrire des preuves avec une dose d'efforts raisonnable, c'est un sujet de recherche actif).


Il y a d'autres outils du même tonneau que je connais mal. Twelf en particulier est réputé pour être un peu plus facile à utiliser (et, en contrepartie, un peu plus restreint et moins généraliste). Agda est très proche du langage Haskell, donc peut être un bon choix si tu connais déjà bien ce langage.

Ensuite il y a des trucs plus exotiques comme Obj/Maude qui ne sont pas vraiment de la preuve formelle, mais qui restent des langages de spécification, et que je ne connais pas de toute façon.

[gasche]

Histoire de donner un exemple concret, voici une preuve Coq de ce que tu donnais en exemple.
J'ai utilisé plus(x,plusun(y)) => plusun(plus(x,y)) au lieu de plus(plusun(x),y) parce que ça rend les preuves plus simples.

Code :

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
Inductive nat : Type :=
| Zero : nat
| Plusun : nat -> nat.

Fixpoint plus (x y : nat) : nat :=
  match y with
    | Zero => x
    | Plusun y' => Plusun (plus x y')
  end.

Lemma plus0 : forall x, plus Zero x = x.
  induction x.
    (* cas  0+0 = 0 *)
      trivial.
    (* cas  0+x = x  =>  0+(x+1) = x+1 *)
      simpl.
      rewrite IHx. (* IHx est ici le nom de l'hypothèse de récurrence *)
      reflexivity.
Qed.

[hellfoust]

Merci bien pour cette réponse très complète.

Ce n'est pas grave si faire des preuves, ça demande du travail et si c'est contraignant pour la programmation. Ca ne me pose aucun problème. Je préfère que ça soit le plus formel possible.

Si j'ai bien compris, on peut écrire un programme en Coq, et faire la preuve de ce programme en Coq aussi. Ca serait super de pouvoir faire les deux dans le même langage ! Mais je me demande si ça ne pose pas des problèmes de complexité. Par exemple, la complexité d'une addition a+b est-elle en O(b) ? (peut-être pas pour les entiers, il y a des bibliothèques, mais est-ce que tu n'es jamais tombé sur un cas ou la complexité passe de constante à polynomiale ?)


Autre question : est-ce qu'on peut écrire les spécifications en Coq, faire les preuves avec Coq, alors que le programme est implémenté avec OCaml/Haskell/... ? Je me doute que la cohérence spécif / programme sera moins bonne. Mais est-ce que l'un des langages fonctionnel de "complexité classique" est plus adapté que les autres pour ce genre de conversion (spécif vers programme, programme vers spécif) ?

[gasche]

Si j'ai bien compris, on peut écrire un programme en Coq, et faire la preuve de ce programme en Coq aussi. Ca serait super de pouvoir faire les deux dans le même langage ! Mais je me demande si ça ne pose pas des problèmes de complexité. Par exemple, la complexité d'une addition a+b est-elle en O(b) ? (peut-être pas pour les entiers, il y a des bibliothèques, mais est-ce que tu n'es jamais tombé sur un cas ou la complexité passe de constante à polynomiale ?)

Je ne comprends pas très bien la question.

Dans mon code, la représentation choisie pour les entiers est une représentation unaire (comme sugérée par ta spécification), donc la complexité de l'addition est effectivement en O(b). Si tu veux une implémentation plus efficace il faut choisir une autre représentation (par exemple en binaire, pour avoir du O(log n)), mais les preuves seront sans doute plus compliquées. Tu pourras ensuite montrer l'équivalence des deux représentations.

De façon générale il y a souvent (mais pas toujours) un compromis à faire entre l'efficacité du programme et la difficulté de la preuve associée.

Autre question : est-ce qu'on peut écrire les spécifications en Coq, faire les preuves avec Coq, alors que le programme est implémenté avec OCaml/Haskell/... ? Je me doute que la cohérence spécif / programme sera moins bonne. Mais est-ce que l'un des langages fonctionnel de "complexité classique" est plus adapté que les autres pour ce genre de conversion (spécif vers programme, programme vers spécif) ?

Le plus simple est de tout faire côté Coq. Il existe des outils pour faire le pont dans les deux sens:
- un mécanisme d'extraction permet, à partir d'un code Coq, de produire du code Caml/Haskell correspondant pour l'exécuter ensuite. Par exemple le compilateur CompCert est un compilateur de C codé en Coq, avec une preuve que la sémantique de l'assembleur produit est bien celle du programme C initial, mais le compilateur concrètement est extrait vers OCaml puis compilé vers du code natif
- il y a des outils pour relier un programme dans un autre langage et une preuve Coq de fonctionnement; par exemple Why, ou plus récemment le travail d'Arthur Charguéraud sur les formules caractéristiques

[hellfoust]

Je vois. Les axiomes de la spécification algébrique servent de code source pour le programme Coq.

A propos de la complexité, je suis d'accord pour rajouter une constante multiplicative (par exemple parcourir trois fois une liste au lieu d'une seule), mais ça me "perturbe" beaucoup plus de passer de O(1) à O(n), ou de O(n) à O(2^n).

Mais bon, c'est le prix à payer on dirait, ou alors on ne peut que prouver que la spécification est juste, sans dire si le programme correspond à la spécification.

Je vais essayer Coq alors, pour la résolution de grilles de sudoku. Merci de m'avoir aiguillé vers cet outil !

[gasche]

Tu as pas mal de liberté dans ce que tu choisis d'implémenter et de prouver. On peut implémenter en Coq des algorithmes efficaces (par exemple Union-find) et prouver leur complexité. Ce que je voulais dire c'est que souvent une implémentation simple, très proche des spécifications, sera plus facile à prouver, mais en contrepartie moins efficace.

[TropMDR]

Bonsoir

Si tu veux te mettre à Coq, je te conseille ce cours: http://www.cis.upenn.edu/~bcpierce/sf/
C'est de loin ce qui se fait de mieux.

Ensuite pour les histoires de complexités : La représentation "à la peano" des entiers est évidement catastrophique pour la complexité, et ne convient pas pour des entiers de taille moyenne (plus que quelques dizaines, maximum).

Mais la librairie standard de coq fournit une représentation binaire des entiers (http://coq.inria.fr/stdlib/Coq.NArith.BinNat.html ), avec donc une additions en O(ln n), ce qui est bien plus raisonnable.

Dans l'état actuel de la qualité des outils, la meilleur solution reste de programmer/prouver en Coq, puis d'extraire le code vers caml. Ca empêche tout programme impératif, mais c'est raisonnablement utilisable !

[hellfoust]

Merci pour le cours.

Pour l'extraction de code vers OCaml, ce n'est pas très utile car je pense que le code généré en OCaml sera aussi lent (algorithmiquement) que le code Coq. Parce que si on optimise à la main le code OCaml, les preuves deviennent obsolètes.

[TropMDR]

Envoyé par hellfoust

Pour l'extraction de code vers OCaml, ce n'est pas très utile car je pense que le code généré en OCaml sera aussi lent (algorithmiquement) que le code Coq.

Bah, pas utile... disons que ça permet d'avoir un programme qui s'exécute hein !

[ceciestunpseudo]

Envoyé par TropMDR

Bah, pas utile... disons que ça permet d'avoir un programme qui s'exécute hein !

Et surtout qui est prouvé valide. Il me semble que c'était aussi un peu le but de la manœuvre non ? Ou alors je n'ai pas compris toute la discussion.