Publicité
+ Répondre à la discussion
Affichage des résultats 1 à 10 sur 10
  1. #1
    Invité de passage
    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 : 0
    Points
    0

    Par défaut Invariant de boucle entrée/sortie

    Bonjour,
    Je dois prouver mon programme big_fermat :


    Code :
    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 Valentin Robert
    Étudiant
    Inscrit en
    juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Nom : Homme Valentin Robert
    Âge : 25
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : juin 2004
    Messages : 70
    Points : 153
    Points
    153

    Par défaut

    Merci d'utiliser de l'indentation et une balise de code afin d'éviter d'abimer mes yeux :

    Code :
    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
    Invité de passage
    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 : 0
    Points
    0

    Par défaut

    Désolé, mais c'était mon premier post donc je le saurais pour la prochaine fois

  4. #4
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    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: le cours OCaml, 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 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

    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 Valentin Robert
    Étudiant
    Inscrit en
    juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Nom : Homme Valentin Robert
    Âge : 25
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : juin 2004
    Messages : 70
    Points : 153
    Points
    153

    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
    Invité de passage
    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 : 0
    Points
    0

    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 :
    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
    Invité de passage
    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 : 0
    Points
    0

    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
    Rédacteur
    Avatar de SpiceGuid
    Homme Profil pro Damien Guichard
    Inscrit en
    juin 2007
    Messages
    1 574
    Détails du profil
    Informations personnelles :
    Nom : Homme Damien Guichard
    Localisation : France, Loire (Rhône Alpes)

    Informations forums :
    Inscription : juin 2007
    Messages : 1 574
    Points : 2 449
    Points
    2 449

    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: le cours OCaml, 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 Valentin Robert
    Étudiant
    Inscrit en
    juin 2004
    Messages
    70
    Détails du profil
    Informations personnelles :
    Nom : Homme Valentin Robert
    Âge : 25
    Localisation : Etats-Unis

    Informations professionnelles :
    Activité : Étudiant

    Informations forums :
    Inscription : juin 2004
    Messages : 70
    Points : 153
    Points
    153

    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.

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
  •