Invariant de boucle entrée/sortie

[martin999999]

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 !

[Ptival]

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|];;

[martin999999]

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

[SpiceGuid]

Ç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.

[gasche]

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

[Ptival]

Envoyé par gasche

(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.

[martin999999]

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 ?

[martin999999]

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

[SpiceGuid]

Envoyé par gasche

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.

[Ptival]

Une petite voix me dit que gasche a déjà rencontré Tony Hoare en personne cette année.

Drôle de remontage de sujet.