Une révolution pour l'industrie du logiciel (c) (TM) - Page 1

http://www.lemonde.fr/web/recherche_articleweb/1,13-0,36-399960,0.html

Jusqu'à présent , les éditeurs de programmes ont eu la "belle vie", selon l'expression de Damien Doligez, chercheur à l'Institut national de recherche en informatique et en automatique (Inria). L'industrie du logiciel n'a en effet jamais eu, au cours des vingt dernières années, à se remettre profondément en cause. Mais elle sera, dans un tout proche avenir, confrontée à une révolution.

C'est rigolo

g rien dit en fait desolé

./1> ben oui, mais bon c'est pas nouveau

ptet que mes cours d'algo // me serviront a qqc un jour

M'enfin tout n'est pas paralelisable.

PpHd> tous les algorithmes, non c'est sûr. Cela dit à une échelle au dessus, il y a toujours moyen de parallèliser en répartissant les tâches. Les programmes dont le rôle est juste de lancer en boucle un et un seul algorithme sur un ensemble de données sont plutôt rares.

il serait ainsi envisageable de programmer des logiciels sans avoir à en écrire directement le code. De telles interfaces graphiques commencent à voir le jour, mais elles sont encore loin de remplir les missions qui pourraient, à l'avenir, leur être assignées, notamment produire du code parallélisé et exempt de bogues.

Il est mal informé visiblement. Les programmes sensibles (sécurité des personnes) ça fait bien longtemps qu'ils ne sont plus écrits à la main (en tous cas partout où la sécurité est capitale). Les programmes qui font marcher le Météor, par exemple, n'ont jamais été touchés par un humain. Le code fait plusieurs millions de lignes, et a été écrit par un ensemble de programmes auxquels des analyses fonctionnelles détaillées ont été fournies. Et il est parallélisé, redondant et tolérant aux pannes (à TOUTES les pannes) par nécessité (c'était dans les specs de départ).

Donc bon l'informatique grand public va s'y mettre peu à peu dans les décennies à venir, mais c'est pas une découverte fracassante.

et il est pas prouvé en Coq ?

spectras :
Il est mal informé visiblement. Les programmes sensibles (sécurité des personnes) ça fait bien longtemps qu'ils ne sont plus écrits à la main (en tous cas partout où la sécurité est capitale). Les programmes qui font marcher le Météor, par exemple, n'ont jamais été touchés par un humain. Le code fait plusieurs millions de lignes, et a été écrit par un ensemble de programmes auxquels des analyses fonctionnelles détaillées ont été fournies.

Enfin c'est un petit peu exagéré, ça : ce n'est pas parce qu'il y a un compilateur C et que donc le code assembleur n'a jamais été touché par un humain que le code C n'a jamais été touché par un humain...

Sauf que là il n'y a pas de code du tout. On a directement donner à manger les analyses SADT.
Autrement dit le boulot a été de faire un cahier des charges complet et détaillé. Une fois ça fait, le programme fait le reste tout seul (euh bon il tourne sur des supercalculateurs aussi, c'est ptet un peu gourmand pour un usage personnel ).
Le principe est un peu le meme que le logiciel sur lequel vince bosse, sauf que l'interface n'est pas un truc improvisé mais des blocs SADT, et que c'est destiné à faires des systèmes complets, pas un logiciel seul. Et pas droit à l'erreur (principe n°1 : tout incident, depuis un bug jusqu'à la surchauffe d'une résistance, depuis une coupure de courant jusqu'à la soudure que se détache, doit conduire à une situation plus sure que le fonctionnement normal).

Et le programme qui fait le reste tout seul, il aurait pas été programmé à la main aussi ?

Et si lui, était bogué ? hein ?
En général pour éviter ça, on utilise la redondance à tous les niveaux.

sauf qu'il y a une partie qui a été prouvée. après, je sais pas comment ça été exactement prouvé (c'est spurque prouver le code C mais pas le compilo/ assembleur, ça sert un peu à rien ...)

Bon pr etre précis ... météor a été analysé avec la méthode SADT puis écrit en langage B (c pas de la prog c des preuves)

120 000 lignes de B ont donné, après 30 000 preuves, dans les 80-90000 lignes de code ADA

=> 1er essai == 0 bugs

pas mal nan ?


ensuite pour les preuves je peux vous donner des exemples mais c pas tres compréhensible ^^

yAro :
Bon pr etre précis ... météor a été analysé avec la méthode SADT puis écrit en langage B (c pas de la prog c des preuves)

Pour etre plus précis, c'est de "l'event B", une variante du B avec une gestion poussée de tout ce qui est évenement (toujours inventée par Jean-Raymond Abrial d'ailleurs ) C'est plus propre que par exemple une approche du type CSP2B ou CSP//B

ben oui, mais bon c'est pas nouveau

L'article prétends pas que c'est nouveau mais pustôt que ça va devenir indispensable à moyen terme car la montée en fréquence commence à montrer ces limites.

je veux dire, c'est pas nouveau que ça va devenir indispensable à moyen terme

Avant c'était plutôt une vision à long terme. Le fait que la course au à la fréquence s'essoufle(même si elle à encore une bonne marge d'évolution) c'est plutôt récent.

>Les programmes dont le rôle est juste de lancer en boucle un et un seul algorithme sur un ensemble de données sont plutôt rares.
Sauf que ce sont en general les plus gourmands

oué
Mais si t'as plusieurs ensemble distincts de données à traiter, tu peux toujours lancer plusieurs traitements en parrallèle.
En plus c'est le plus simple à faire, y'a même pas besoin de retoucher au programme.

dans le cas ou il s'agit de bloc de donnée distincts oui mais ce n'est malheureusement pas toujours faisable facilement de travailler en bloc distincs.

edit: j'avais pas fait attention au "distinct"

./12 : non, parce qu'ils ont utilisé l'ADA, donc c'est mal(tm)