Aujourd'hui on utilise les algorithmes bayésiens pour créer des filtres antispam qui fonctionnent relativement bien ( bon ils ont des limites qui ont pu être démontrées lors de la dernière conférence sur le spam au MIT en 2004 par JCG ), mais pourquoi se limiter aux filtres antispam ? Le code source ( C ou autre langage ) est un langage, on dispose aujourd'hui avec les cvs, les diff des différents logiciels libres d'une formidable base de données de corrections de bugs. On pourrait peut être appliqué cette méthode à la recherche de bugs dans les codes source ? C'est peut être une idée complètement stupide, mais pourquoi ne pas essayer ? Un BO, c'est quasiment toujours la même chose, ça se voit dans le source, on peut donc, en modélisant au niveau du compilateur un niveau d'abstraction suffisant, créer un analyseur ( et résolveur ) de bugs assez puissant. On parle aujourd'hui beaucoup des problèmes de sécurité un peu partout, mais pourquoi ne pas essayer cette solution pour venir à bout de ces problèmes de programmation ??? C'est un peu plus complexe parce que ça ne porte pas seulement sur un token, mais sur un ensemble, un n-uplet avec des contraintes associées mais ça reste possible... Si des personnes sont intéressées pour m'aider à développer ça ( ou simplement et modestement dans un premier temps, montrer que ça peut fonctionner ), elles peuvent me contacter, je pourrais leur expliquer plus en détail. J'ai vu sur le net que certaines personnes pensent que c'est complètement loufoque, mais bon avant d'essayer et de tester, je n'ai pas envie de partir perdant, et je préfère penser que ça peut fonctionner, et si jamais c'est le cas, c'est génial et ça sera une nouvelle victoire du logiciel libre sur le logiciel propriétaire... ( je ne cherche pas à lancer un nouveau débat, mais le logiciel libre est là, c'est une source d'informations formidable et autant s'en servir et apporter une modeste contribution à ce dernier ). Et pour finir "Free software, free society", une bien belle idée à l'heure de la societé d'information...
( allez on va encore dire que je délire, -1, mais non il faut essayer avant... l'explication donnée ici est simpliste, mais ce n'est peut être pas aussi simple à modéliser et coder, mais si ça fonctionne, c'est le bingo assuré... ).
Journal Bayes appliqué au code ?
13
mai
2004
# Je comprend pas...
Posté par ploum (site web personnel, Mastodon) . Évalué à 3.
Je veux un pion vert sur un pion rouge, pas l'inverse : c'est un bug
Chouette, je voulais un pion rouge sur un pion vert : ça marche
Comment tu vas expliquer au filtre bayésien ce que tu attend de ton programme pour qu'il sache si c'est un bug ou non ?
ça c'est le premier problème.
Admettons que tu aies un bug qui fasse boucler ton programme.
Le filtre bayésien peut détecter ce bug. Donc HALT
Donc, ce filtre bayésien est impossibe ... CQFD ;)
Mes livres CC By-SA : https://ploum.net/livres.html
[^] # Re: Je comprend pas...
Posté par Nap . Évalué à 0.
En spécialisant par métier, comme il le dit lui-même (exemple : les applis de BO), tu veux toujours un pion rouge sur un pion vert...
Je dis ça pour défendre ses arguments, même si moi j'y crois pas trop :)
Admettons que tu aies un bug qui fasse boucler ton programme.
Le filtre bayésien peut détecter ce bug. Donc HALT
Donc, ce filtre bayésien est impossibe ... CQFD ;)
j'ai rien compris :)
[^] # Re: Je comprend pas...
Posté par ploum (site web personnel, Mastodon) . Évalué à 2.
On a démontré que c'était impossible et c'est très utile afin de savoir ce qui est possible ou pas.
Mais, y'a toujours des gens pour chercher, chercher et prétendre avoir la réponse.
Je suis pour les recherches a priori loufoques. Mais celles dont on peut démontrer dès le départ qu'elles sont impossibles sans remettre en cause une majorité de la science actuelle me semble généralement une perte de temps. Je ne crois pas au mouvement perpétuel, la démonstration m'en semble évidente. Et si qqn l'invente un jour, toute la mécanique, thermondynamique, etc sera donc fausse ! (ce que l'expérience contredit).
En logiciel, il en est de même pour halt. Son idée se résumant en gros à HALT, je ne dis pas qu'elle n'apportera pas peut-être certaines choses, mais je parie beaucoup qu'elle n'aura en tout cas jamais l'effet escompté.
Mes livres CC By-SA : https://ploum.net/livres.html
[^] # Re: Je comprend pas...
Posté par tene . Évalué à 5.
Petite précision pour ceux qui ont pas tout compris, la fonction HALT serait une fonction à laquelle on fournit un programme et elle on aurait le résultat "vrai" si le programme se termine, et "faux" si le programme ne se termine jamais... C'est en effet impossible à faire... (et ça se démontre) mais:
Une approcha bayesienne est originale par le fait qu'elle se base sur des probabilités et non pas des certitudes... dans le même ordre d'idée, bien que HALT soit impossible pour tout les programmes, il est possible de le faire pour certains programmes, c'est ce qui arrive parfois d'ailleurs, le compilo nous crache un beau warning signalant que tel partie ne sera jamais exécuté parce que la boucle est infinie...
Cependant, je ne pense pas que l'idée puisse mener à grand chose, perso je vois 2 trucs:
- détecter des patterns (par exemple l'emploi d'une fonction sprintf qui est souvent source de trou de sécurité par buffer overflow). Ca se fait depuis longtemps, ça donne une appréciation du code... dans certaines boites c'est même spécifié et tester de façon formelle, via un ensembel de règle.
- Appliquer la méthode bayesienne à un code source n'est pas un problème, tout comme pour le spam, c'est une façon de classer des données en deux ensembles (spam ou non, ou "bon programme", "mauvais programme")... le vrai problème c'est de traiter les données en entrée pour avoir un "bon format"... et dans le cas d'un code source, beaucoup (trop) de chose dépendent du programme (nom de variable, etc...).
En bref le vrai problème est celui des patterns: comment les définir, lesquelle choisir, etc... peut-être l'auteur de la news y a déjà réfléchi?
[^] # Re: Je comprend pas...
Posté par Marc (site web personnel) . Évalué à 1.
Fallait dire ça aux gens qui justement ont chercher dans le sens de la thermo, ils allaient un peu contre les idées du moment. Je suis pas sûr que la relativité était généralisée au moment où elle a été présenté... c'est con mais bon...
[^] # Re: Je comprend pas...
Posté par yaya . Évalué à 1.
l'expérience ne peut pas contredire une invalidation de théorie...
[^] # Re: Je comprend pas...
Posté par Ze Fredz . Évalué à 2.
Prends l'exemple de l'algorithme de vérification des classes Java. Que fait-il ? En analysant le bytecode d'une classe Java, il décide si ce code est valide ou non. Or ceci revient à déterminer une caractéristique d'un programme, ce qui est impossible si on tient compte de la fonction HALT (et du théorème de l'arrêt et de toute la théorie de la calculabilité).
Or cet algorithme existe bel et bien. Comment est-ce possible ? En fait ce qui se passe c'est que le vérificateur de bytecode est susceptible de refuser une classe Java bien formée. C'est là qu'intervient la fonction HALT.
Ce que dit la calculabilité ce n'est pas qu'il est impossible de créer un algorithme qui calcul une propriété d'unj programme, mais qu'il est impossible de créer un algorithme qui calcule cette propriété avec une certitude absolue !
Dans le cas du vérificateur de bytecode Java, les concepteurs de la JVM ont mis des règles plus restrictives que celles nécessaires pour qu'une classe Java soit valide. Conséquence : de temps en temps une classe est refusée bien que parfaitement valide et sans danger (remarque : cela n'apparaît que chez les gens qui travaillent directement en assembleur pour la JVM, par exemple dans le cadre d'un TFE avec BOBO... Le compilateur Java ne produit, lui, que du bytecode valide)
Donc le risque du filtre bayésien pour les bugs est que si les règles ne sont pas suffisamment restrictives, il ne détecte pas certains bugs, et, dans le cas contraire, il détecte certains bugs qui n'en sont pas.
Mais il est donc bel et bien possible de créer un tel filtre imparfait. Et puis il y a toujours moyen de faire appel à un oracle : l'utilisateur (dans le cas de la JVM, l'oracle c'est le switch "-noverify" qui court-circuite l'algorithme de vérification).
Cette recherche n'est donc pas aussi loufoque qu'elle n'y paraît, sinon adieu aux vérificateurs de code, aux optimiseurs, aux antivirus,...
[^] # Re: Je comprend pas...
Posté par fmaz fmaz . Évalué à 4.
C'est du même genre que les gens qui disent que comme un problème est montré NP-complet, il ne sert à rien d'essayer de le résoudre.
Ce qu'il veux faire, ce n'est certainement pas resoudre le problème de la HALT en général. C'est résoudre le problème de la halt sur une classe la plus grande possible de programmes. Tu sais, moi je sais résoudre la halt pour les fonctions récursives primitives. Fondamentalement, quand un compilateur te sort un avertissement, c'est qu'il pense que tu es en train de faire une connerie.
« attention, t'es pas en train de confondre égalité et affectation dans ton if? »
Je ne sais pas si son approche est possible mais ce n'est à priori pas fondamentalement idiot.
# Idée
Posté par Infernal Quack (site web personnel) . Évalué à 5.
L'association LinuxFr ne saurait être tenue responsable des propos légalement repréhensibles ou faisant allusion à l'évêque de Rome, au chef de l'Église catholique romaine ou au chef temporel de l'État du Vatican et se trouvant dans ce commentaire
# Recherche fondamentale
Posté par pllevy . Évalué à 3.
Tu as raison de te lancer dans l'aventure, au pire "il ya toujours à apprendre de ses échecs".
Ce sera sans moi car je ne pourrais pas beaucoup t'aider, mais je te souhaite bon courage !
# Bien plus interessant
Posté par ckyl . Évalué à 1.
http://www.stanford.edu/~engler/(...)
http://coverity.com/main.html(...)
J'ai au moins vu passer des messages d'eux sur lkml et freebsd-hackers...
Par contre je ne sais pas si une partie du projet est libre...
# The Cooperative Bug Isolation Project
Posté par jmfayard . Évalué à 3.
http://www.cs.berkeley.edu/~liblit/sampler/(...)
A toi de me dire comment ça marche parceque je n'ai personellement rien compris ;-)
[^] # Re: The Cooperative Bug Isolation Project
Posté par scoubid00 . Évalué à 1.
# ca existe presque deja
Posté par Mouns (site web personnel) . Évalué à 1.
aujourd'hui, pour certains languages, cela s'appelle la preuve formelle ( genre http://www.idealx.org/doc/intro_preuve_formelle.fr.html(...) ).
le principe est simple :
prouver que le programme fait ce qu'il doit faire si :
1 - l'environnement est suffisament bug free
2 - que le developpeur sait coder ce qu'il voulait coder
3 - que le codeur sait exprimer au demontreur que qu'il doit demontrer
maintenant, ca ne marche pas pour tout.
Suivre le flux des commentaires
Note : les commentaires appartiennent à celles et ceux qui les ont postés. Nous n’en sommes pas responsables.