Forum de mathématiques - Bibm@th.net

Marc-Antoine

Invité

algorithme d'optimisation

Amis des nombres , bien le bonjour...

Juste une petite question à vous soumettre.
Existe t-il une méthode standard permettant de démontrer qu'un algorithme donné rend bien en sortie le résultat pour lequel il a été créé ?

Je vous remercie par avance pour vos réponses...

freddy

Membre chevronné

Lieu : Paris

Inscription : 27-03-2009

Messages : 7 457

Re : algorithme d'optimisation

Salut,

ben oui, ça s'appelle faire une recette : pour des cas dont tu connais la solution, l'algo doit donner la même solution, sinon ... Parfois, il en fournit d'autres, c'est à ce moment là que ça devient intéressant, sportif, et que tu commences à perdre ton sommeil, voire ta raison !

Marc-Antoine

Invité

Re : algorithme d'optimisation

Merci pour ton attention ,

Justement je cherche une démonstration plus forte que celle par l'exemple , car l'algorithme peut être efficace sur tous les exemples qu'on lui a proposé, ça ne démontre en rien qu'il le sera pour tous les exemples qu'on lui proposera...

La seule interprétation que je puisse faire pour l'heure a partir de l'algorithme , c'est de le décortiquer en expliquant sa genèse , mais cela n'a toujours aucune valeur démonstrative...

Pour le coup , le mot est parfaitement choisi, c 'est sportif !!! limite je deviens fou en fait ..

yoshi

Modo Ferox

Inscription : 20-11-2005

Messages : 17 385

Re : algorithme d'optimisation

Bonjour,

Nous avons de temps en temps un dénommé Barbichu qui passe et au point question Maths (issu de Cachan) et programmation.
Il a à plusieurs reprises évoqué ici même le langage Coq : il me semble que c'est peut-être là, la réponse à ta question...
http://www.bibmath.net/forums/viewtopic.php?id=4766&p=2
http://www.bibmath.net/forums/viewtopic … 222#p36222 post #45 en réponse à mon post #44...

Va voir du côté de ce sympathique gallinacé...

Coq est fondé sur le calcul des constructions (introduit par Thierry Coquand, CoC abrégé en anglais, d'où un jeu de mots justifiant le nom du système), une théorie des types d'ordre supérieur, et son langage de spécification est donc une forme de lambda-calcul typé. Le calcul des constructions utilisé dans Coq comprend directement les constructions inductives, d'où son nom de calcul des constructions inductives (CIC).

Coq a été récemment doté de fonctionnalités d'automatisation croissantes. Citons notamment la tactique Omega qui décide l'arithmétique de Presburger1

Plus particulièrement, Coq permet :

    de manipuler des assertions du calcul ;
    de vérifier mécaniquement des preuves de ces assertions ;
    d'aider à la recherche de preuves formelles ;
    de synthétiser des programmes certifiés à partir de preuves constructives de leurs spécifications.

C'est un logiciel libre distribué selon les termes de la licence GNU LGPL.

Parmi les grands succès de Coq, on peut citer:

    théorème des quatre couleurs: la démonstration complètement mécanisée a été terminée en 2004 par Georges Gonthier et Benjamin Werner.
    Théorème de Feit et Thompson: la preuve du théorème a été terminée par Georges Gonthier et son équipe en septembre 20122.
    CompCert un compilateur optimisant le C (langage) qui est entièrement programmé et prouvé en Coq.

Site : http://coq.inria.fr/

Sinon, en quelques cas précis, on doit pouvoir faire la preuve d'un algorithme qui doit rendre un résultat chiffré, en lui fournissant une variable (ou plus) et en faisant le boulot pas à pas "à la main"...

@+

Marc-Antoine

Invité

Re : algorithme d'optimisation

Merci pour ta réponse, je regarde tout ça dès ce soir

Barbichu

Membre actif

Inscription : 15-12-2007

Messages : 405

Re : algorithme d'optimisation

Bonjour Marc-Antoine, Yoshi,

Nous avons de temps en temps un dénommé Barbichu qui passe et au point question Maths (issu de Cachan) et programmation.
Il a à plusieurs reprises évoqué ici même le langage Coq : il me semble que c'est peut-être là, la réponse à ta question...

[…]

Sinon, en quelques cas précis, on doit pouvoir faire la preuve d'un algorithme qui doit rendre un résultat chiffré, en lui fournissant une variable (ou plus) et en faisant le boulot pas à pas "à la main"...

Avant d'aller faire de la preuve formelle assistée par ordinateur il y a du paysage à visiter. On peut commencer à parler de correction d'algorithme sur papier. Dans les incontournable, il y a la Logique de Hoare. À partir de là on peut aussi s’intéresser à des aspects plus spécifiques des langages de programmation (utilisation de la mémoire, sémantique opérationnelle, dénotationnelle, etc …), ou à des aspects spécifiques aux algorithmes qu'on étudie.

Quant à l'étude informatisé de correction de programmes, il y a les ancêtres tels que la méthode B et des tentatives plus modernes telles que Why3 et beaucoup d'autres que je ne cite pas.
Bien sûr Coq permet aussi d'aborder le problème, mais n'est pas vraiment spécialisé dans la preuve de programme.

A+

Dernière modification par Barbichu (28-10-2013 19:16:14)