Reprise du message précédent :

c'est un truc à la con de sodomites matheus en somme    
 
 
(humour)

Non: Si c'etait pas si lourd, ca permettrait de verifier la logique de ce que l'on code. Peut etre que dans le futur, ca sera integre dans les compilos qui te previendront des erreurs de logique d'un programme...
A+,

Clarkent a écrit a écrit : tu veux dire un invariant ?

 
tout a fait... tu demandera a mon tube d'aspirine vide pkoi je me suis planté

C'est bien beau de "prouver" un algorithme dans la théorie...
...mais faudrait pas oublier que la programmation est dans le domaine pratique !
 
Introduisez la chronologie, les interruptions, les entrées utilisateur, et il ne reste plus beaucoup de certitudes.
 
PS: Les pointeurs c'est dangereusement puissant et j'aime ça.

 
Une preuve si elle n'est pas complete n'est pas interessante !
 
on peut prouver une programme qui utilise
des pointeurs, comme on peut prouver un programme qui utilise des gotos. Par exemple je suis parti de la definition complete de mon parseur, j'en ai deduit l'implementation qui sauf erreur de frappe est une implementation correcte de ce que j'avais prevu (avec des gotos). A comparer a une experience qui consiste a partir de rien, de coder directement, de tester sur deux exemples pour voir si ca les reconnait bien et de releaser le code (..et disparaitre avec la caisse).
 
De meme les avioniques (instruments embarquees) disposent de langages de description qui permettent de prouver avec les hypotheses de depart (programmation temps reel), l'algo retranscrit dans le langage.
Evidemment ca n'empechera pas le concepteur de faire des erreurs de logique. Aucun systeme n'est infaillible et on sera evidemment bien inspire de faire des tests complets derriere.  
(cf l'experience d'Ariane)
 
La "pratique" ca ne veut pas dire 1=2!
 
LeGreg

OUI c'est utile.
 
Tres meme.
 
Car il ne faut pas oublier que votre experience de la programmation n'est pas l'experience de tout le monde et surtout ne represente pas la totalite de la programmation.
 
Pour moi, c'est d'une importance capitale dans les domaines serieux. Prouver que sa fonction est correcte permet d'eviter des erreurs graves, conduisant parfois a des catastrophes, dans des endroits ou cela est requis.
 
Imaginez les programmesdecontrole d'une centrale nucleaire ecris en C sans preuve par un gars sortant de la fac. Ca vous ferai peur hein ? Ben moi aussi.
 
La preuve est quelque chose d'extremement puissant permettant de valider un algorithme.
 
C'est tres difficile a mettre en place, surtout a cause des boucles.
 
Utilisez un language fonctionnel et cela deviens deja beaucoup plus facile (preuve par recurrence dans ce cas).
 
La programmation c'est pas seulement faire une appli qui va afficher une jolie boiboite ou programmer un joli chat en ligne en php/javascript sa race.
 
C'est aussi faire voler des avions, aller dans l'espace, et meme faire vivre des gens, dans les hopitaux.
 
Donc, le moindre bug peux etre fatal. Tous les outils pour les virer dans ces cas doivent etre utilises. La preuve par Hoare triple est un des outils les plus puissants disponibles a ce jour.
 
Pourquoi s'en priver ?
 
a+

 
 
ben c'est simple:a un matheux, il lui faut 1mois pour calculer le cout, alors qu'il faut 1 jour pour programmer l'algo et se rendre compte que le truc rame a fond.
 
idem pour les algo (sur les graphes par exemple): un mateux va te trouver la solution parfaite en 6mois alors que toi tu trouves une solution assez bonne en 3 jours...

je nie pas l'interet de la theorie quand on cherche un theoreme. mais quand on cherche une solution pratique, faut des praticiens: c'est tout.
 
 
chui plus padawan   ?

parce que c'est tres lourd, parce que ça demande énormément de temps, parce que ça n'empèche en aucun cas d'avoir des bugs, parce que les langages fonctionnels ne sont utilisés que par les "sodomites matheus" (ce terme me fait mourir de rire, désolé ), etc...

Ah oui ? Un seul exemple, spécial franciliens : le RER A.
 
Au milieu des années 90, la RATP a décidé d'augmenter au maximum la fréquence des RER A dans Paris (en heures de pointe) tout en garantissant une sécurité totale des personnes transportées. Objectif : qu'un train arrive en gare toutes 2 minutes (et ce pour toutes les stations intra muros). Or les conducteurs ne peuvent en aucun cas assurer un tel débit : les risques de collision dans le cas où un train serait obligé de s'arrêter sont énormes.
La RATP a donc décider de faire conduire ces trains par du logiciel, et pour garantir un zéro défaut dans le logiciel, donc zéro accident = zéro mort chez les passagers, elle a exigé que le bon fonctionnement du coeur de ce logiciel soit prouvé. Mathématiquement. Ce qui a été fait : à ma connaissance, ce sont près de 25 000 des 80 000 lignes du soft de gestion du RER A qui ont été prouvés mathématiquement.
Et chaque jour, le RER A transporte ainsi des centaines de milliers de personnes avec un débit au bord de la rupture, sans que jamais un seul accident ne se soit produit depuis que ce logiciel a été mis en service...
 
PS: Je vous rassure, je n'ai pas d'actions dans la RATP...  

BifaceMcLeOD a écrit a écrit :   Ah oui ? Un seul exemple, spécial franciliens : le RER A.   Au milieu des années 90, la RATP a décidé d'augmenter au maximum la fréquence des RER A dans Paris (en heures de pointe) tout en garantissant une sécurité totale des personnes transportées. Objectif : qu'un train arrive en gare toutes 2 minutes (et ce pour toutes les stations intra muros). Or les conducteurs ne peuvent en aucun cas assurer un tel débit : les risques de collision dans le cas où un train serait obligé de s'arrêter sont énormes. La RATP a donc décider de faire conduire ces trains par du logiciel, et pour garantir un zéro défaut dans le logiciel, donc zéro accident = zéro mort chez les passagers, elle a exigé que le bon fonctionnement du coeur de ce logiciel soit prouvé. Mathématiquement. Ce qui a été fait : à ma connaissance, ce sont près de 25 000 des 80 000 lignes du soft de gestion du RER A qui ont été prouvés mathématiquement. Et chaque jour, le RER A transporte ainsi des centaines de milliers de personnes avec un débit au bord de la rupture, sans que jamais un seul accident ne se soit produit depuis que ce logiciel a été mis en service...   PS: Je vous rassure, je n'ai pas d'actions dans la RATP...

Est-ce que le logiciel qui pilote la ligne D du metro de lyon a été prouvé lui aussi ? depuis 10 ans qu'il fonctionne il n'a pas eu d'accident non plus    
 
Est-ce que le logiciel qui pilotait la première Ariane 5 a été prouvé lui aussi ? parce que si c'est le cas, c'est la preuve que la preuve mathématique d'un programme ne garantit pas l'absence de bug.

alors celon toi, en 6 mois, un mathematicien trouverait l algo exacte pour que ca marche (exemple pour lancer une fusee), et toi en 3 jours tu as une soluce a peu pret bonne (exemple pour faire decole une fusee, je crois que t auras surement trouver le moyen de la faire s ecraser et la ton algo sera 100% bon, c est sur que tu seras alle plus vite que le matheux pour trouver comment la faire atterir ).

mais je te parle pas de trucs vitaux ou de temps réels.
 
exemple: emploi du temps d'un etablissement scolaire. si on prends l'algo d'un matheu pour avoir le meilleur emploi du temps, ben tu peux attendre la rentrée suivante (vu le temps CPU qu'il va falloir, rien que ce la)
 
par contre avec un algo glouton, c'est fait tout de suite

les matheux come tu disent prennent en compte la complexite de l algo ce que toi apaprement tu ne fais pas. il trouvera surement un algo bien plus rapide que le tient.

mareek a écrit a écrit : Est-ce que le logiciel qui pilote la ligne D du metro de lyon a été prouvé lui aussi ? depuis 10 ans qu'il fonctionne il n'a pas eu d'accident non plus       Est-ce que le logiciel qui pilotait la première Ariane 5 a été prouvé lui aussi ? parce que si c'est le cas, c'est la preuve que la preuve mathématique d'un programme ne garantit pas l'absence de bug.

Très amusantes, tes remarques. «Si c'est pô une preuve, ça, hein, bon...», diront certains...
Franchement, si tu n'as que ça comme argument bidon, tu as le droit de t'abstenir.

Je signale à tous les programmeurs qui méprisent les mathématiciens que sans ces mêmes mathématiciens, l'ensemble des supports sur lesquels vous travaillez n'existeraient même pas : Boole, Babbage, von Neumann, Knuth, ... pour n'en citer que quelques uns.

certain programmes sans reflechir, ils perdent du temps a coriger les cas qu'il n avaient jamais prevu.
d'autres prevoient un minimum, puis n'ont plus qu a taper le code et ca roule, certain ont du mal a le comprendre ca .

Manifestement tu ne connais pas les matheux en question et tu n'as aucune idée de leur boulot et encore moins de leur utilité ...

Clarkent a écrit a écrit : certain programmes sans reflechir, ils perdent du temps a coriger les cas qu'il n avaient jamais prevu. d'autres prevoient un minimum, puis n'ont plus qu a taper le code et ca roule, certain ont du mal a le comprendre ca .

on doit pas connaitre les mêmes chercheurs  

BifaceMcLeOD a écrit a écrit :   Très amusantes, tes remarques. «Si c'est pô une preuve, ça, hein, bon...», diront certains... Franchement, si tu n'as que ça comme argument bidon, tu as le droit de t'abstenir.

qu'est-ce qu'ils ont mes exemples ? ils ont autant de valeur que ton exemple de la RATP.

mareek a écrit a écrit : on doit pas connaitre les mêmes chercheurs

et toi t ess ur de comprendre ce queje dis .

Clarkent a écrit a écrit : et toi t ess ur de comprendre ce queje dis .

je suis pas sûr d'avoir compris ton précédent post justement

mais biensur que je les connais: mais le boulot des mathématiciens, ca se compte en décénie. dans la pratique faut arreter de se la mordre et avancer.

alors serts toi des outils qu'ils ont cree pour te simplifier la vie .

Clarkent a écrit a écrit : alors serts toi des outils qu'ils ont cree pour te simplifier la vie .

 
j'aime pas les matheu c'est pas des geeks

 
oui malheureusement, il faut des decennies pour que les outils mis en place par les theoriciens (mathematiciens ou informaticiens puisque maintenant l'info est une discipline a part entiere, il manque juste un concours separe dans l'education nationale francaise) soient utilises en large part dans les programmes informatiques. Faut dire que les informaticiens moyens meprisent toute connaissance qui n'est pas mise sous la forme d'un tutorial, alors le temps que quelqu'un comprenne et mette un tutorial a disposition il y a le temps .
 
Quelques grands theoriciens (de ce siecle ou d'ailleurs):
Edeger Dijkstra,
Alan Turing,
Ada Lovelace,
Charles Babbages,  
John Von Neuman,  
Donald Knuth,  
Alan Newell,
Claude Shannon etc..
 
Et pour un domaine qui me concerne (le graphisme ):
Gouraud, Lambert, Bezier, Blinn, Hoppe, Sillion, Catmull, Mandelbrot, Descartes etc..
 
LeGreg

je connais tous les premiers    
 
mais quan dje vois les chercheurs dans ma fac, ni pedagogue ni programmeur, j'ai du mal a voir en eux un avenir

Taz@PPC a écrit a écrit : je connais tous les premiers       mais quan dje vois les chercheurs dans ma fac, ni pedagogue ni programmeur, j'ai du mal a voir en eux un avenir

chercheur ca ne veut aps dire pedagogue ni programmeur ni autre chose, ca veut dire chercheur.

 
ben alors pourquoi ils enseignent?. bon, on peut aprler d'autre chose, je commence a saturer la

bein ils enseignent a la fac, la fac c est pas la reunion des pedagogue et des enseignants supers competents qui font ca par passion .
ils sont oblige d enseigne s ils veulent faire de la recherche, ils en ont rien a taper de ta vie.
enfin pas tous, beaucoup sont tres sympas et prennent leur taffe au serieux, d autres se font chier lorsqu'ils font les cours et ne pensent qu a ce qu ils vont faire juste apres pour leur recherche.

legreg a écrit a écrit :     Et pour un domaine qui me concerne (le graphisme ): Gouraud, Lambert, Bezier, Blinn, Hoppe, Sillion, Catmull, Mandelbrot, Descartes etc..   LeGreg

J'ai pas aimé son dernier film.

 
Faudra se sortir du crâne un jour que "informatique = programmation" ...
 
Ceci dit dans ma fac y'avait des gars qui etaient bons chercheurs (dans des domaines qui meme pour toi sont de l'informatique : théorie de la compilation), bons profs et bons développeurs (au point de venir se faire démarcher par l'industrie dans son propre bureau).

mareek a écrit a écrit : Est-ce que le logiciel qui pilote la ligne D du metro de lyon a été prouvé lui aussi ? depuis 10 ans qu'il fonctionne il n'a pas eu d'accident non plus       Est-ce que le logiciel qui pilotait la première Ariane 5 a été prouvé lui aussi ? parce que si c'est le cas, c'est la preuve que la preuve mathématique d'un programme ne garantit pas l'absence de bug.

 
pour ariane la acuse etait differente, c just eke les anglais ont pas capter ke le systeme universelle, c le system metrik...

c'est marrant, on m'a dit que le problème venait d'un morceau de code provenant du programme pilotage (c'est surement pas le vrai nom, mais tout le monde me comprendra) d'Ariane 4 qui n'était pas prévu pour gérer les accélérations d'Ariane 5 et qui avait planté.
 
Enfin, ça ne change rien à ce que je voulais dire, que le programme soit prouvé ou non, une catastrophe peut toujours se produire.

 
je crois que tu confonds Ariane 5
avec Mars Climate Orbiter..
 
LeGreg

 
j'avais lu ca concernant le premier vol d'ariane 5 c sur... apres par contre ca fait longtemps je c plus ou g lu ca... mais g un copai ki bosse sur A5 a kourou je lui demanderai

 
A ma connaissance le bout de code en question n'avait pas ete prouve. Le module inertiel (IRS) etait garanti fonctionable (comme l'ont prouve les nombreux lancers reussis d'Ariane 4). Seulement la garantie venait a une condition qui n'etait pas respectee sur Ariane 5 effectivement.
 
J'ai des connaissances qui travaillent ici:
http://www.polyspace.com/
Je crois qu'ils embauchent
 
LeGreg

Le rapport d'enquête (je sens que la logique de Hoare s'éloigne !) :
 
http://www.cnes.fr/espace_pro/comm [...] t_501.html

legreg a écrit a écrit : A ma connaissance le bout de code en question n'avait pas ete prouve. Le module inertiel (IRS) etait garanti fonctionable (comme l'ont prouve les nombreux lancers reussis d'Ariane 4). Seulement la garantie venait a une condition qui n'etait pas respectee sur Ariane 5 effectivement.   J'ai des connaissances qui travaillent ici: http://www.polyspace.com/ Je crois qu'ils embauchent   LeGreg

Mais si ce bout de code avait été prouvé, est-ce que ça aurait changé qqch ? le pb ne venait pas de l'algo en lui même mais plutot des données qu'il a reçu.

 
Tout aurait ete preferable a ne pas le tester du tout..
 
LeGreg