IdentifiantMot de passe
Loading...
Mot de passe oublié ?Je m'inscris ! (gratuit)
Navigation

Inscrivez-vous gratuitement
pour pouvoir participer, suivre les réponses en temps réel, voter pour les messages, poser vos propres questions et recevoir la newsletter

Caml Discussion :

Invariant de boucle entrée/sortie


Sujet :

Caml

  1. #1
    Candidat au Club
    Homme Profil pro
    Étudiant
    Inscrit en
    Mars 2012
    Messages
    5
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Paris (Île de France)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : Mars 2012
    Messages : 5
    Points : 2
    Points
    2
    Par défaut Invariant de boucle entrée/sortie
    Bonjour,
    Je dois prouver mon programme big_fermat :


    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    let big_fermat n =
      if n egale deux then [| un ; deux |] else
      let x = ref ((deux fois (racine n)) plus un)
      and r = ref (((racine n) fois (racine n)) moins n)
      and y = ref un in
        while not (!r egale zero) do begin
            if !r superieur_a zero then
              begin
                r := !r moins !y;
                y := !y plus deux;
              end
            else if !r inferieur_a zero then
              begin
                r := !r plus !x;
                x := !x plus deux;
              end
            else () end done;
        let aux1 = ((!x moins !y) divisé_par deux)
        and aux2 = ((!x plus !y moins deux) divisé_par deux) in
          [|aux1; aux2|];;
    Je dois donc trouver les invariants de boucles en entrée et en sortie, mais la je ne vois pas trop ...
    Est ce que quelqu'un pourrait m'aider ?

    PS : je travaille en big_int ,sur caml light, et j'ai redefini toutes les fonctions prédéfinies sur caml light pour rendre le programme plus clair.
    Ex : J'ai defini racine comme sqrt_big_int.

    Merci d'avance !

  2. #2
    Membre actif
    Avatar de Ptival
    Homme Profil pro
    Étudiant
    Inscrit en
    Juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 35
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : Juin 2004
    Messages : 70
    Points : 276
    Points
    276
    Par défaut
    Merci d'utiliser de l'indentation et une balise de code afin d'éviter d'abimer mes yeux :

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
    9
    10
    11
    12
    13
    14
    15
    16
    17
    18
    19
    20
    21
    22
    23
     
    let big_fermat n =
      if n egale deux
      then [| un ; deux |]
      else
        let x = ref ((deux fois (racine n)) plus un)
        and r = ref (((racine n) fois (racine n)) moins n)
        and y = ref un in
        while not (!r egale zero) do begin
          if !r superieur_a zero then
          begin
            r := !r moins !y;
            y := !y plus deux;
          end
          else if !r inferieur_a zero then
          begin
            r := !r plus !x;
            x := !x plus deux;
          end
          else () end done;
        let aux1 = ((!x moins !y) divisé_par deux)
        and aux2 = ((!x plus !y moins deux) divisé_par deux) in
        [|aux1; aux2|];;

  3. #3
    Candidat au Club
    Homme Profil pro
    Étudiant
    Inscrit en
    Mars 2012
    Messages
    5
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Paris (Île de France)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : Mars 2012
    Messages : 5
    Points : 2
    Points
    2
    Par défaut
    Désolé, mais c'était mon premier post donc je le saurais pour la prochaine fois

  4. #4
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    Juin 2007
    Messages
    1 704
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : Juin 2007
    Messages : 1 704
    Points : 2 990
    Points
    2 990
    Par défaut
    Ça n'est pas un problème de langage mais plutôt un exercice d'algorithmie.
    On appelle ça de la programmation par contrat et d'habitude c'est Eiffel le langage de référence pour ce genre d'exercice.
    C'est pourquoi je ne saurais trop te recommander la lecture de :
    Introduction a la théorie des langages de programmation, InterEditions, 1992 par Bertrand Meyer
    Tu devrais trouver cet ouvrage à la bibliothèque de ton établissement.
    Il y a un chapitre consacré aux boucles et à leur vérification (pseudo-)formelle.
    Plus précisément:
    • il y a une phase d'initialisation qui doit garantir l'invariant ainsi qu'une valeur positive pour le variant
    • il y a un invariant de boucle qui doit rester vrai durant toute l'itération
    • pour prouver la terminaison il y également un variant de boucle qui doit être positif et strictement décroissant, la boucle se termine quand ce variant atteint la valeur zéro

    Tu trouveras plus d'explications ainsi que des exemples de code (et de "preuve") dans l'ouvrage mentionné ci-dessus.
    Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  5. #5
    Membre éprouvé
    Profil pro
    Inscrit en
    Avril 2007
    Messages
    832
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Avril 2007
    Messages : 832
    Points : 1 104
    Points
    1 104
    Par défaut
    Je trouve un peu abusif de dire que c'est Eiffel la référence en la matière d'invariants de boucle. Des preuves de programmes par préservation d'invariant on en fait depuis longtemps, les papiers de Knuth, Dijkstra ou Hoare en sont remplis, c'est bien connu et bien maîtrisé (comme technique de preuve manuelle) depuis longtemps.


    (Par contre je trouve que la question est trop mal posée et c'est pour ça que je n'y ai pas répondue. On nous demande d'aider à prouver un programme sans expliquer son fonctionnement ou même dire ce qu'il est censé faire, et le code ne donne pas envie d'être lu, sauf pour les gens qui trouvent que "r", "x" et "y" c'est le summum de la clarté comme nom de variables...)

  6. #6
    Membre actif
    Avatar de Ptival
    Homme Profil pro
    Étudiant
    Inscrit en
    Juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 35
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : Juin 2004
    Messages : 70
    Points : 276
    Points
    276
    Par défaut
    Citation Envoyé par gasche Voir le message
    (Par contre je trouve que la question est trop mal posée et c'est pour ça que je n'y ai pas répondue. On nous demande d'aider à prouver un programme sans expliquer son fonctionnement ou même dire ce qu'il est censé faire, et le code ne donne pas envie d'être lu, sauf pour les gens qui trouvent que "r", "x" et "y" c'est le summum de la clarté comme nom de variables...)
    Pareil. Le seul indice dans ton code c'est "big_fermat", et je n'ai pas envie de chercher le rapport entre ça et ton code.

    Pour trouver un invariant de boucle, il "faut" (c'est mieux) comprendre ce que la boucle essaie de faire (et comment elle essaie de le faire). L'invariant est une formule qui est vraie au moment où on entre dans la boucle, et rétablie à chaque tour de boucle. Il faut donc que tu trouves une propriété (non triviale) qui est vraie au moment où tu entres dans la boucle, et qui est vraie après exécution du corps de la boucle en faisant l'hypothèse qu'elle est vraie au début du corps de la boucle.

  7. #7
    Candidat au Club
    Homme Profil pro
    Étudiant
    Inscrit en
    Mars 2012
    Messages
    5
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Paris (Île de France)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : Mars 2012
    Messages : 5
    Points : 2
    Points
    2
    Par défaut
    Désolé de ne pas avoir été plus clair !

    Ce programme sert à décomposer un entier en facteur de deux nombres, pas forcément premier.
    Par contre si le nombre de départ n est premier, le programme rend [ 1; n ] .

    On peut facilement en déduire une façon de décomposer un nombre en facteur premier :

    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    let rec dec n = 
       let aux = big_fermat n in 
         if hd aux = 1 then aux else 
         (dec (hd aux))@(dec(hd(tl aux))) ;;
    Ce programme me sert dans le cadre d'un travail sur la methode RSA ou il faut décomposer la clé publique en deux facteur premier etc ...
    Est-ce plus clair comme ça ?

  8. #8
    Candidat au Club
    Homme Profil pro
    Étudiant
    Inscrit en
    Mars 2012
    Messages
    5
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Paris (Île de France)

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : Mars 2012
    Messages : 5
    Points : 2
    Points
    2
    Par défaut
    Petite rectification dans le programme dec :
    dans le cas ou hd aux = 1 il faut renvoyer "tl aux" et non "aux" pour ne pas voir apparaître les 1 dans la decomposition en facteurs premiers.

    De plus big_fermat ne marche que pour des nombres impairs.

    En ce qui concerne le nom de ce programme : Il s'agit d'un algorithme trouvé par Pierre de Fermat. de plus je travaille en big_int donc :
    => big_fermat

  9. #9
    Membre émérite
    Avatar de SpiceGuid
    Homme Profil pro
    Inscrit en
    Juin 2007
    Messages
    1 704
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : Juin 2007
    Messages : 1 704
    Points : 2 990
    Points
    2 990
    Par défaut
    Citation Envoyé par gasche Voir le message
    Je trouve un peu abusif de dire que c'est Eiffel la référence en la matière d'invariants de boucle. Des preuves de programmes par préservation d'invariant on en fait depuis longtemps, les papiers de Knuth, Dijkstra ou Hoare en sont remplis, c'est bien connu et bien maîtrisé (comme technique de preuve manuelle) depuis longtemps.
    Tu as 100% raison.

    Seulement si tu es un inculte et que tu veux trouver des citations (TAGS) de Dijkstra ou Hoare hé bien tu vas sur le blog de l'auteur d'Eiffel.

    Pareil si tu veux voir Hoare en chair et en os tu te rends à une conférence de la ETH Chair of Software Engineering à laquelle Hoare a été invité par la même personne.
    Du même auteur: mon projet, le dernier article publié, le blog dvp et le jeu vidéo.
    Avant de poser une question je lis les règles du forum.

  10. #10
    Membre actif
    Avatar de Ptival
    Homme Profil pro
    Étudiant
    Inscrit en
    Juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Sexe : Homme
    Âge : 35
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : Juin 2004
    Messages : 70
    Points : 276
    Points
    276
    Par défaut
    Une petite voix me dit que gasche a déjà rencontré Tony Hoare en personne cette année.

    Drôle de remontage de sujet.

Discussions similaires

  1. Données d'Entrée - Sortie - Test - Boucle
    Par edmond dans le forum Langages de programmation
    Réponses: 2
    Dernier message: 20/12/2007, 09h58
  2. [Débutant]Procédure avec paramètres entrée / sortie
    Par jeromejanson dans le forum Langage
    Réponses: 13
    Dernier message: 10/10/2005, 09h30
  3. Débutant - Entrée/Sortie
    Par seigneur.viggen dans le forum Langage
    Réponses: 11
    Dernier message: 28/09/2005, 16h47
  4. Copie entrée-sortie
    Par Troell dans le forum C
    Réponses: 18
    Dernier message: 24/09/2005, 20h11
  5. Réponses: 11
    Dernier message: 13/10/2004, 01h58

Partager

Partager
  • Envoyer la discussion sur Viadeo
  • Envoyer la discussion sur Twitter
  • Envoyer la discussion sur Google
  • Envoyer la discussion sur Facebook
  • Envoyer la discussion sur Digg
  • Envoyer la discussion sur Delicious
  • Envoyer la discussion sur MySpace
  • Envoyer la discussion sur Yahoo