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

Algorithmes et structures de données Discussion :

Demontrer l'exactitude d'un algorithme


Sujet :

Algorithmes et structures de données

  1. #1
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut Demontrer l'exactitude d'un algorithme
    Que doit on faire exactement quand on doit montrer qu'un algo est correct?

    Ce n'est pas quand même prendre un exemple, vérifier pour trouver le résultat!

  2. #2
    Membre averti Avatar de elmcherqui
    Profil pro
    Inscrit en
    Février 2008
    Messages
    281
    Détails du profil
    Informations personnelles :
    Âge : 36
    Localisation : Maroc

    Informations forums :
    Inscription : Février 2008
    Messages : 281
    Points : 382
    Points
    382
    Par défaut
    - verifier d'abord si il donne les resultats qu'on attend de lui .
    - si oui voir si il est robuste c.a.d qu'il gere un maximum de cas , a toi de trouver les cas les plus tordu et extremes (a la main bien sur ) .
    - et enfin optimiser si optimisation il y'a .

  3. #3
    Rédacteur

    Avatar de millie
    Profil pro
    Inscrit en
    Juin 2006
    Messages
    7 015
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2006
    Messages : 7 015
    Points : 9 818
    Points
    9 818
    Par défaut
    Salut nathy,

    Tu cherches à trouver s'il y a des chances que l'algo soit correct (tests etc.) ou à prouver formellement que ce soit correct (donc preuve avec des outils comme PVS, coq) ?
    Je ne répondrai à aucune question technique en privé

  4. #4
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut bsr elmcherqui
    Optimiser un algorithme !!
    i.e. ameliorer veux tu dire?
    merci

  5. #5
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut bsr millie
    merci pour ton intervention
    le probleme est juste poser prouver que cette algo est correct
    je ne connais ces tests dont tu parles.
    Je ne suis pas une informaticienne (Pvs,coq...je ne sais pas de quoi il s 'agit ).

  6. #6
    Rédacteur

    Avatar de millie
    Profil pro
    Inscrit en
    Juin 2006
    Messages
    7 015
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2006
    Messages : 7 015
    Points : 9 818
    Points
    9 818
    Par défaut
    Citation Envoyé par nathy810 Voir le message
    merci pour ton intervention
    le probleme est juste poser prouver que cette algo est correct

    Je ne suis pas une informaticienne (Pvs,coq...je ne sais pas de quoi il s 'agit ).

    je ne connais ces tests dont tu parles.
    Je parle de tests unitaires, mais cela concerne forcement une implémentation de l'algorithme dans un langage. Donc, on teste l'implémentation sur un ensemble de valeur déterminé.
    Par exemple, si j'ai une fonction qui retourne le carré d'un entier, on va tester quelques valeurs : carre(0) == 0 ?, carre(2) == 4 ? ... On teste souvent les cas normaux, les cas limites et les cas d'erreurs.


    Pour la partie preuve, il y a plusieurs méthodes.
    Soit on prouve l'algorithme à la main (si l'algorithme est écrit sous forme récursive, c'est plus simple, s'il est écrit sous forme impérative, c'est un peu plus compliqué).
    Soit on prouve l'algorithme à l'aide de logiciel qui permettent de vérifier que ta preuve est bonne (il faut obligatoirement avoir une idée de la preuve avant de se lancer là dedans...) :
    Par exemple Coq : http://coq.inria.fr/coq-fra.html
    PVS : http://pvs.csl.sri.com/
    A noter que ces outils permettent plus généralement de voir si une preuve est juste (n'importe quel preuve mathématiques).

    C'est souvent assez délicat de comprendre comment ces outils fonctionnent et il faut pas mal d'entrainement pour savoir comment faire.

    Je n'ai personnellement utilisé que PVS, j'ai tenté une fois coq, mais j'avais un peu de mal. J'ai déjà également utilisé un autre outil pour prouver des algorithmes écrit sous forme impératives, mais j'ai oublié le nom...
    Je ne répondrai à aucune question technique en privé

  7. #7
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut merci
    Saurait tu ce qu'on entend par invariant de boucle?
    Serait ce les variables qui dans une boucle n evolue pas au fil des calculs ou bien quoi
    merci

  8. #8
    Rédacteur

    Avatar de millie
    Profil pro
    Inscrit en
    Juin 2006
    Messages
    7 015
    Détails du profil
    Informations personnelles :
    Localisation : France

    Informations forums :
    Inscription : Juin 2006
    Messages : 7 015
    Points : 9 818
    Points
    9 818
    Par défaut
    Citation Envoyé par nathy810 Voir le message
    Saurait tu ce qu'on entend par invariant de boucle?
    Serait ce les variables qui dans une boucle n evolue pas au fil des calculs ou bien quoi
    merci
    C'est une propriété valable tout le long du déroulement d'une boucle ou d'appel récursif.

    Par exemple :
    Code : Sélectionner tout - Visualiser dans une fenêtre à part
    1
    2
    3
    4
    5
    6
    7
    8
     
    fonction somme(entier n) {
      entier s = 0;
      Pour i = 1 à n {
         s = s + i;
      }
      retourner s;
    }
    Dans la boucle, tu as la propriété pour les entiers (i,n,s) qui dit que : Somme des k de 1 à i = s.
    C'est un invariant de boucle.

    A à la fin, tu as i=n, donc tu peux montrer que s est égal à Somme des k de 1 à n.
    Je ne répondrai à aucune question technique en privé

  9. #9
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut merci encore millie mais je te pose encore une question
    est ce a dire que l'invariant de boucle est ce que je j'obtiens a la sortie de ma boucle.
    Et s'il me faut verifier que certaines conditions sont des invariantes de boucles,je reprends juste le resultat retourner et je verifie dans ces conditions?
    Ce que je fais est purement mathematique mais l informatique que je retrouve dedans me perds
    je ne suis pas calée en info hein!
    merci

  10. #10
    Membre du Club
    Profil pro
    Inscrit en
    Juillet 2005
    Messages
    55
    Détails du profil
    Informations personnelles :
    Âge : 40
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations forums :
    Inscription : Juillet 2005
    Messages : 55
    Points : 61
    Points
    61
    Par défaut
    Salut,

    a noter que ton invariant de boucle est une propriété qui doit etre vraie à 4 endroits :

    - Avant de rentrer dans la boucle
    - Au début de la boucle
    - A la fin de la boucle (c'est-a-dire juste avant d'effectuer le test de sortie de boucle)
    - Après la boucle

    La difficulté c'est donc de trouver l'invariant surtout si la boucle est complexe.

  11. #11
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut salut cedriku
    moi jai un algo ou je dois je crois trouver l invariant de boucle et meme montrer qu il est invariant de boucle

  12. #12
    Membre du Club
    Profil pro
    Inscrit en
    Juillet 2005
    Messages
    55
    Détails du profil
    Informations personnelles :
    Âge : 40
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations forums :
    Inscription : Juillet 2005
    Messages : 55
    Points : 61
    Points
    61
    Par défaut
    Si t'arrives vraiment pas a voir, montre nous ton algo, dis nous ce que tu pense etre un invariant.

  13. #13
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut
    cet algo je l'ai redigé suite a bcp d'autres questions precedentes
    en supposant donc que je l'ai trouvé

    c:=b^t mod (p);
    r=a^(t+1)/2 mod p;
    Pour i=1 à s-1 faire
    d=[(r^2)a^-1]^2^(s-i-1);
    tant que d<>1 mod p faire
    r:=r*c mod(p);
    c:=c^2 mod p;
    fintantq
    finpour
    retourner(r,-r)

    l'invariant de boucle est il r:=r*c.
    en fait je ne sais pas encore vraiment mais je soumets deja mon algo
    je reecris ds un instant si j ai kelke chose de nouveau

  14. #14
    Membre du Club
    Profil pro
    Inscrit en
    Juillet 2005
    Messages
    55
    Détails du profil
    Informations personnelles :
    Âge : 40
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations forums :
    Inscription : Juillet 2005
    Messages : 55
    Points : 61
    Points
    61
    Par défaut
    Bon, dejà pour etre clair, est ce que c'est :

    r=(a^(t+1))/2 mod p
    ou bien
    r=a^((t+1)/2) mod p

    pour savoir si le 2 est dans la puissance ou c'est le tout sur 2 ?

    Ensuite ou se termine ta boucle Pour ? (je suppose juste avant le tant que mais suis pas sur)

    Ensuite il y a un probleme pour ta boucle Tant Que :

    Tu dis tant que d<>1... or d ne change jamais de valeur dans la boucle, donc si tu y rentre la premiere fois, tu n'en sortiras jamais (d sera toujours different de 1) -> boucle infinie. Donc ceci me fait penser que finalement la boucle Tant Que est imbriqué dans la boucle Pour ???

    Indique bien les fin de tes boucle avec FinPour ou FinTantQue par exemple car sinon on ne sait pas si elle sont imbriquées ou pas...

    Autre chose, donnes les spécification de ton algo, c'est-à-dire, les données en entrées (je suppose que c'est a,b,p, s et t), et le resultat que ca doit renvoyer !

  15. #15
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut
    c est ceci pour etre bien precise
    r=[a^((t+1)/2)]mod p

    le 2 est dans la puissance


    Ensuite ou se termine ta boucle Pour ? (je suppose juste avant le tant que mais suis pas sur)
    Non tant que est dans ma boucle pour
    en fait j ai mis finpour en dessous vois tu?

    Ensuite il y a un probleme pour ta boucle Tant Que :

    Tu dis tant que d<>1... or d ne change jamais de valeur dans la boucle, donc si tu y rentre la premiere fois, tu n'en sortiras jamais (d sera toujours different de 1) -> boucle infinie. Donc ceci me fait penser que finalement la boucle Tant Que est imbriqué dans la boucle Pour ???
    elle est imbriquée comme tu dis
    je teste si d est 1 je n entre pas dans tantque et sinon d evolue avec le i

    Indique bien les fin de tes boucle avec FinPour ou FinTantQue par exemple car sinon on ne sait pas si elle sont imbriquées ou pas...

    tu as eu mon message non achevé
    je reeditais encore

    les resultats d'est r et -r
    en entrees je prends juste p et a
    les autres variables sont juste calculées
    bien sur que je les declare
    (t,s,d,c,b)
    j avais a une fiche precedente ecrit une fonction qui retrouve t et s avec un p premier donné.

    bon je crois que c est un peu plus clair

  16. #16
    Membre du Club
    Profil pro
    Inscrit en
    Juillet 2005
    Messages
    55
    Détails du profil
    Informations personnelles :
    Âge : 40
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations forums :
    Inscription : Juillet 2005
    Messages : 55
    Points : 61
    Points
    61
    Par défaut
    Citation Envoyé par nathy810
    elle est imbriquée comme tu dis
    je teste si d est 1 je n entre pas dans tantque et sinon d evolue avec le i
    Oui mais imagine tu rentre dans la boucle Tant Que, dans cette boucle, seuls r et c sont modifiés donc le test d<>1 sera toujours vrai et tu n'en sortira jamais !!! Le seul endroit ou d est modifié c'est en dehors de la boucle Tant Que...

  17. #17
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut un invariant est
    je veux trouver les racines de a mod p
    est ce que je peux dire que a=r^2 est un invariant de boucle
    je crois que ce doit etre verifier a chaque fois dans mon algo
    quitte a le verifier je vais chercher a montrer
    je me demande donc now si un seul suffit?
    merci

  18. #18
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut
    je vais modifier un truc dans mon algo encore

    c:=b^t mod (p);
    r=a^(t+1)/2 mod p;
    Pour i=1 à s-1 faire
    d=[(r^2)a^-1]^2^(s-i-1);
    si d<>1 mod p faire
    r:=r*c mod(p);
    c:=c^2 mod p;
    finsi
    finpour
    retourner(r,-r)

  19. #19
    Membre du Club
    Profil pro
    Inscrit en
    Juillet 2005
    Messages
    55
    Détails du profil
    Informations personnelles :
    Âge : 40
    Localisation : France, Bouches du Rhône (Provence Alpes Côte d'Azur)

    Informations forums :
    Inscription : Juillet 2005
    Messages : 55
    Points : 61
    Points
    61
    Par défaut
    Citation Envoyé par nathy810
    je vais modifier un truc dans mon algo encore

    c:=b^t mod (p);
    r=a^(t+1)/2 mod p;
    Pour i=1 à s-1 faire
    d=[(r^2)a^-1]^2^(s-i-1);
    si d<>1 mod p faire
    r:=r*c mod(p);
    c:=c^2 mod p;
    finsi
    finpour
    retourner(r,-r)
    Bon deja, le fait de mettre un Si plutot que Tant Que, c'est bien mieux (je sais pas si c'est juste par rapport au calcul que tu veux faire mais au moins t'as plus de boucle infinie...).

    Ca simplifiera également la preuve plutot que d'avoir deux boucles imbriquées.



    Citation Envoyé par nathy810 Voir le message
    est ce que je peux dire que a=r^2 est un invariant de boucle
    C'est pas possible que a=r^2 soit invariant car dans la boucle a ne change jamais alors que r oui.

  20. #20
    Nouveau Candidat au Club
    Inscrit en
    Décembre 2008
    Messages
    12
    Détails du profil
    Informations forums :
    Inscription : Décembre 2008
    Messages : 12
    Points : 1
    Points
    1
    Par défaut
    mais la je crois que je n ai pas bien pigé ce que c est qu un invariant.
    je viens de lire un exemple
    l'algo d euclide
    ils disent que a=B*Q+R est un invariant de boucle alors qu ici aussi a ne change pas dans la boucle tantque

    B := b;
    R := a;
    Q := 0;
    Tant que R ≥ B faire
    R := R − B ;
    Q := Q + 1 ;
    fintq ;

    je dois encore bien cerner la notion "invariant de boucle"
    ou alors tu aimerais que je dise r^2=a
    ca va?
    [/COLOR]

Discussions similaires

  1. Formalisation graphique des algorithmes
    Par David R. dans le forum Algorithmes et structures de données
    Réponses: 14
    Dernier message: 08/12/2012, 11h21
  2. Algorithme de randomisation ... ( Hasard ...? )
    Par Anonymous dans le forum Assembleur
    Réponses: 8
    Dernier message: 06/09/2002, 15h25
  3. recherches des cours ou des explications sur les algorithmes
    Par Marcus2211 dans le forum Algorithmes et structures de données
    Réponses: 6
    Dernier message: 19/05/2002, 23h18
  4. Recherche de documentation complète en algorithmes
    Par Anonymous dans le forum Algorithmes et structures de données
    Réponses: 1
    Dernier message: 29/03/2002, 13h09
  5. Algorithme génétique
    Par Stephane.P_(dis Postef) dans le forum Algorithmes et structures de données
    Réponses: 2
    Dernier message: 15/03/2002, 18h14

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