Reprise du message précédent :

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

 
mais un code prouvé a plus de chances de savoir avant de s'executer si oui ou nom il pourra arriver au bout...  
 
dans la preuve on justifie et le fait kil finisse et le fait ke le resultat soit bon...
et ya des conditions pour ca... elles se testent avant l'execution... dc ca aurait pu changer kke chose

je suis en train de lire et c'est assez hallucinant comme une petite erreur à la con dans un bout de code isolé peut avoir comme répercutions. En gros, l'erreur vient d'une erreur de conversion d'un flotant 64 bits en entier 16 bits dans un bout de code qui n'est plus utile après le décollage (mais qui tourne quand même). Quand je pense que ça a même pas été testé correctement  

Mouais ... moi je ne suis pas assuré et je ne mets pas ma ceinture, mais ca ne change rien, tant que je n'ai pas d'accident ...

Gonzoide a écrit a écrit :   Mouais ... moi je ne suis pas assuré et je ne mets pas ma ceinture, mais ca ne change rien, tant que je n'ai pas d'accident ...

merci de ta contribution, mais ça ne réponds pas à ma question

L'absence de preuve ne prouve rien, ni le vrai ni le faux. Donc ce n'est pas parce que le bon fonctionnement d'un logiciel -- en l'occurrence, le métro de Lyon -- n'a pas été prouvé mathématiquement qu'il contient des bugs. Simplement on ne le sait pas (s'il en contient).
 
Je te signale au passage que les conditions d'utilisation du métro de Lyon sont différentes de celles du RER A parisien ; et tu ne sais pas quelles sont les contraintes sur le logiciel. Les 2 logiciels ne sont tous simplement pas comparables.
En tout cas, à Paris, les contraintes qui reposent sur le logiciel du RER A sont uniques : aucune autre des 5 lignes de RER, ni aucune autre ligne de métro (il y en a 14) n'a de telles contraintes (une rame toutes les 2 minutes, une vitesse de croisière entre 2 stations de 70 à 80 km/h, permettant un débit de plusieurs milliers de personnes par minute pendant plusieurs heures non-stop, 2 fois par jour).
 
Par ailleurs, concernant ton 2ème exemple, je constate que tu pars d'une supposition. Or à ma connaissance, le logiciel d'Ariane 5 n'a jamais été prouvé (à moins que tu ne me prouves le contraire, bien sûr ). Mais avec des suppositions comme celles-là, on peut raconter n'importe quoi...    
 
mareek> Si je me souviens bien, le logiciel n'a pas planté, il a considéré que la valeur d'accélération horizontale était en dehors des bornes admises, et que malgré les alertes qu'il déclenchait à la centrale de commande des moteurs, cette valeur restait bien au-delà des valeurs permises. Le problème c'est que la valeur en question était invalide seulement pour le petit bout de code de mesure et de contrôle de cette valeur, pas pour la centrale. Donc la centrale ne corrigeait rien, puisque par ailleurs tout était correct.
Le module de mesure et de contrôle de l'accélération horizontale de la fusée, constatant que la fusée continuait à "dériver" (enfin c'est ce qu'il croyait), a estimé qu'elle était en perdition et, comme cela lui était permis, a décidé de faire exploser la fusée en vol, pour éviter qu'elle ne s'écrase sur des zones habitées.

mareek a écrit a écrit :   je suis en train de lire et c'est assez hallucinant comme une petite erreur à la con dans un bout de code isolé peut avoir comme répercutions. En gros, l'erreur vient d'une erreur de conversion d'un flotant 64 bits en entier 16 bits dans un bout de code qui n'est plus utile après le décollage (mais qui tourne quand même). Quand je pense que ça a même pas été testé correctement

Les 3 erreurs les plus coûteuses de l'histoire de la programmation ont été trouvées dans des programmes qui avaient été testés longuement, et relus/vérifiés par un autre programmeur que leur auteur ; et dans les 3 cas, il a suffi de changer un seul chiffre pour corriger l'erreur. Si je me souviens bien, la plus coûteuse de toutes a coûté dans les 250 millions de dollars. Pour un seul chiffre.

Les bogues ordinaires des logiciels très répandus sont très coûteux aussi, par le total de temps de travail perdu par des millions d'utilisateurs.
 
Comme c'est dilué, tout le monde en paye un peu et on ne se rend pas compte du ravage.

BifaceMcLeOD a écrit a écrit :   L'absence de preuve ne prouve rien, ni le vrai ni le faux. Donc ce n'est pas parce que le bon fonctionnement d'un logiciel -- en l'occurrence, le métro de Lyon -- n'a pas été prouvé mathématiquement qu'il contient des bugs. Simplement on ne le sait pas (s'il en contient).   Je te signale au passage que les conditions d'utilisation du métro de Lyon sont différentes de celles du RER A parisien ; et tu ne sais pas quelles sont les contraintes sur le logiciel. Les 2 logiciels ne sont tous simplement pas comparables. En tout cas, à Paris, les contraintes qui reposent sur le logiciel du RER A sont uniques : aucune autre des 5 lignes de RER, ni aucune autre ligne de métro (il y en a 14) n'a de telles contraintes (une rame toutes les 2 minutes, une vitesse de croisière entre 2 stations de 70 à 80 km/h, permettant un débit de plusieurs milliers de personnes par minute pendant plusieurs heures non-stop, 2 fois par jour).   Par ailleurs, concernant ton 2ème exemple, je constate que tu pars d'une supposition. Or à ma connaissance, le logiciel d'Ariane 5 n'a jamais été prouvé (à moins que tu ne me prouves le contraire, bien sûr ). Mais avec des suppositions comme celles-là, on peut raconter n'importe quoi...       mareek> Si je me souviens bien, le logiciel n'a pas planté, il a considéré que la valeur d'accélération horizontale était en dehors des bornes admises, et que malgré les alertes qu'il déclenchait à la centrale de commande des moteurs, cette valeur restait bien au-delà des valeurs permises. Le problème c'est que la valeur en question était invalide seulement pour le petit bout de code de mesure et de contrôle de cette valeur, pas pour la centrale. Donc la centrale ne corrigeait rien, puisque par ailleurs tout était correct. Le module de mesure et de contrôle de l'accélération horizontale de la fusée, constatant que la fusée continuait à "dériver" (enfin c'est ce qu'il croyait), a estimé qu'elle était en perdition et, comme cela lui était permis, a décidé de faire exploser la fusée en vol, pour éviter qu'elle ne s'écrase sur des zones habitées.

 
 
juste un detail dont personne na rien a foutre: 16 lignes de metro, tu as oulier 3bis et 7bis

Tiens, je trouve que les bons programmes devraient être subventionnés.
 
 
Bon, au sujet des méthodes esotériques de prouver un algorithme: C'est très utile.
 
Quand on résoud des problèmes ardus, les moyens mis en oeuvre atteignent une telle complexité qu'on ne peut pas en avoir une compréhension d'ensemble dans la tête.
Il faut alors des méthodes de validation dont on sait qu'elles marchent, même si on ne les comprends pas.
 
Il y a longtemps que ça marche comme ça en mathématique, physique, chimie, ect... L'informatique est à la traine, elle est trop jeune.
 
 
Ce qui m'amènes à des questions...

• Peut-on faire marcher ces outils à l'envers, c'est à dire leur faire générer des algorithmes qui sont par définition prouvés ?

• Pourrait-on se baser dessus pour concevoir un reformulateur d'algorithme, capable de transformer du code sans jamais se tromper ?

Je dirais plutôt que son image est incorrecte. La physique, la chimie sont vues comme des disciplines (à part entière), l'informatique n'est vue que comme un outil. D'ailleurs "tout le monde fait de l'informatique", c'est bien connu... (vous n'avez jamais entendu ça d'un type qui se contente de faire des programmes de 20-30 lignes en Visual Basic ? Moi si : la première fois, ça fait bizarre...)
 
Résultat : la fantastique complexité de la programmation n'est absolument pas prise en compte par la plupart des décideurs ( et en particulier par ceux qui savent faire des programmes de 20-30 lignes).
 

Je pense que oui, avec des techniques relativement proches de celles utilisées pour la démonstration automatique de théorèmes. Le problème, c'est que comme pour la classe de théorèmes automatiquement démontrables, la classe d'algorithmes automatiquement "écrivables" doit être assez limitée...
 

Aujourd'hui, cela existe, mais de manière limitée. Et cela dépend fortement du langage utilisé (certains offrent une syntaxe qui garantit l'absence d'effets de bord dans tel ou tel cas endroit ou sur telle ou telle variable).
Ainsi, par exemple, Occam est un langage qui permet d'écrire assez simplement des algorithmes massivement parallèles (globalement, il existe 2 types de blocs d'instructions : le bloc séquentiel qui correspond au begin/end habituel et le bloc parallèle où toutes les instructions sont exécutées concurremment). Et le compilateur Occam est capable de réécrire avec le maximum de blocs parallèles possible tout algorithme qui exprimé exclusivement à l'aide de blocs séquentiels.
 
Mais de manière générale, tant que les programmeurs réclameront des langages souples et aux possibilités d'effets de bords multiples et variées, les compilateurs ne pourront pas faire de réécriture automatique poussée. Suivez mon regard...  

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

 
Oui c vrai.
 
La RATP utilise le langage B et l'atelier de langage B pour ses dev informatiks. C la même chose pour Eole et Météor (ligne 14) sans conducteur.  
 
Mais bon c vrai qu'il ne faut pas non plus mélanger les besoins de l'informatik de gestion et de l'informatique tps réel ou embarqué. C po les mêmes risques.
 
Enfin si on arrive à créer des AGL de plus en plus intelligent utilisant la logique de Hoare, on peut vraisemblablement se dire que dans quelques temps (15 ans => 100 ans) on aura plus besoin de développeurs.

ça m'arrangerais si cétait plutot dans 100 ans que dans 15

bah, je propose qu'on fonde une societe secrete dont le but serait d'assurer la survie de la caste des programmeurs..
 
de toute facon, peu de gens comprennent ce qu'on fait vraiment alors ce serait facile au fond
 
qu'en pensez-vous?
 
LeGreg

voici un exemple des techniques qui ont ete
utilise sur le logiciel Ariane 5  
 
http://www.irisa.fr/manifestations [...] /15oct.pdf
 
C'est un pdf.
 
LeGreg

mareek a écrit a écrit : ça m'arrangerais si cétait plutot dans 100 ans que dans 15

Bah, m'en fgout, au départ je suis mathématicien, je n'aurai qu'à revenir à mes premières armes !

Et recommencer à réfléchir ! Quelle horreur !  

charly007 a écrit a écrit :   Et recommencer à réfléchir ! Quelle horreur !

il est vraiq ue ca fait longtemps que t as arrete.
Charly007 cherche emploi en tant qu'admin mangeur de beignet.

Bah, il faudra toujours du talent, de l'art et de la jugeotte.
Autant de choses qui ne sont pas près d'être mises en formules.
 
Le métier de développeur changera un peu plus, et la fracture sera encore plus grande entre ceux qui cliquettent dans de beaux logiciels, et ceux qui les concoivent.
 
 
Sans aller jusqu'à la preuve, une organisation saine avec un bon découpage et de puissantes abstractions permet déjà de rendre les choses limpides.

 
Ha bon que ce n'est pas parce que l'on possède Dreamweaver et quelques connaissances en PHP, qu'on peut se définir comme un pro de la création de site web?

Hé bé non.
Pour être de qualité, un produit doit être conçu.
Et pour bien concevoir, il faut comprendre.
 
On n'a pas encore trouvé mieux...

 
En quoi ca consiste et comment ca marche, ca?

En gros, on se repose sur les axiomes de la logique du premier ordre, et on utilise des moteurs d'inférence (c'est-à-dire des softs qui sont capables de tirer des conclusions logiques. Genre avec "si a alors b" et "si b alors c", le soft est capable de conclure "si a alors c" ).