Publicité
+ Répondre à la discussion
Affichage des résultats 1 à 11 sur 11
  1. #1
    Membre actif
    Inscrit en
    janvier 2007
    Messages
    248
    Détails du profil
    Informations forums :
    Inscription : janvier 2007
    Messages : 248
    Points : 150
    Points
    150

    Par défaut Spécification et preuve formelle

    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.

  2. #2
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 009
    Points
    1 009

    Par défaut

    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.

  3. #3
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 009
    Points
    1 009

    Par défaut

    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.

  4. #4
    Membre actif
    Inscrit en
    janvier 2007
    Messages
    248
    Détails du profil
    Informations forums :
    Inscription : janvier 2007
    Messages : 248
    Points : 150
    Points
    150

    Par défaut

    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) ?

  5. #5
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 009
    Points
    1 009

    Par défaut

    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

  6. #6
    Membre actif
    Inscrit en
    janvier 2007
    Messages
    248
    Détails du profil
    Informations forums :
    Inscription : janvier 2007
    Messages : 248
    Points : 150
    Points
    150

    Par défaut

    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 !

  7. #7
    Membre Expert
    Inscrit en
    avril 2007
    Messages
    831
    Détails du profil
    Informations forums :
    Inscription : avril 2007
    Messages : 831
    Points : 1 009
    Points
    1 009

    Par défaut

    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.

  8. #8
    Membre chevronné
    Inscrit en
    mars 2010
    Messages
    281
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 281
    Points : 756
    Points
    756

    Par défaut

    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 !

  9. #9
    Membre actif
    Inscrit en
    janvier 2007
    Messages
    248
    Détails du profil
    Informations forums :
    Inscription : janvier 2007
    Messages : 248
    Points : 150
    Points
    150

    Par défaut

    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.

  10. #10
    Membre chevronné
    Inscrit en
    mars 2010
    Messages
    281
    Détails du profil
    Informations forums :
    Inscription : mars 2010
    Messages : 281
    Points : 756
    Points
    756

    Par défaut

    Citation Envoyé par hellfoust Voir le message
    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 !

  11. #11
    Membre du Club
    Inscrit en
    août 2009
    Messages
    38
    Détails du profil
    Informations forums :
    Inscription : août 2009
    Messages : 38
    Points : 51
    Points
    51

    Par défaut

    Citation Envoyé par TropMDR Voir le message
    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.

+ Répondre à la discussion
Cette discussion est résolue.

Liens sociaux

Règles de messages

  • Vous ne pouvez pas créer de nouvelles discussions
  • Vous ne pouvez pas envoyer des réponses
  • Vous ne pouvez pas envoyer des pièces jointes
  • Vous ne pouvez pas modifier vos messages
  •