ɹǝıʌıʃO a écrit 373 commentaires

J'ai l'impression qu'il y une différence entre les pratiques habituelles pour le développement live critical et ce que tu crois l'être...Les applications live critical (je suppose que tu entends par là life critical, dans la grande tradition francophone de l'emprunt inutile de mots anglais avec autant de fautes que de mots) incluent le contrôle de réacteurs nucléaires, la spécialités de mes formateurs en test de logiciels. C'est un domaine dans lequel on ne se contente pas d'écrire des papiers, et pour avoir habité près de ce genre d'installations, je n'en suis pas fâché.

Ça peut continuer longtemps comme ça...

tu trouves à la main des vecteurs d'entrée, tu évalue ce que doivent être tes sorties et tu compares avec la sortie de ton code.Tu vis en 1970 ?

Dans le cas du test, tu es limité par les vecteurs d'entrée que tu trouves à la main alors qu'avec un moteur de preuve, tu as l'exhaustivité.Pour écrire ça, il faut :
* soit ne pas avoir lu ce que j'ai écrit juste avant ;
* soit choisir délibérément de n'en tenir aucun compte.

Bref, je laisse tomber. Comme dirait l'autre, ma patience a des limites, mais faut pas exagérer.

J'ai donné les deux définitions, qui sont clairement différentes. Pour ceux qui dorment au fond [,qui écrivent sans avoir lu et qui moinssent à la vue du nom de l'auteur], voici un exemple très simple. Le bug de l'instruction FDIV du Pentium 1, pourtant réalisée par un algorithme pour lequel il existe une preuve de correction, était dû à l'absence de certaines entrées dans une table de valeurs précalculées.

Pour la preuve, ceci n'existe pas. Lorsqu'il y a une table de valeurs précalculées dans une preuve, cette table est une constante. Vérifier que toutes les valeurs y sont n'a guère de sens puisque ça revient à écrire l'assertion selon laquelle une constante est égale à elle-même.

Du point de vue des tests (après coup, bien sûr, c'est toujours plus facile), il aurait fallu un test par entrée de la table. Comme le test porte sur la table produite et non sa spécification, ce n'est plus équivalent à une opération nulle.

C'est un exemple-jouet, bien sûr, mais c'est déjà suffisant pour montrer que la preuve de programmes et le test sont deux disciplines différentes qui s'intéressent à deux choses différentes. Il n'y a clairement pas d'inclusion de l'une dans l'autre. Après, on peut remarquer tant qu'on veut qu'elles utilisent des méthodes similaires : on utilise des automates aussi en traitement automatique des langues, pourtant je n'ai entendu personne déclarer que le TAL est inclus dans la preuve de programmes. Pas encore, du moins.

Dire
Je dis simplement que la vérification est supérieure aux testsPour enchaîner sur
pour ce qui est de la supériorité c'est une interprêtation abusive de ta part du mot. Je l'ai exprimé comme un surensemble.C'est au minimum minimorum une formulation vraiment très maladroite. Plus vraisemblablement, de la grosse mauvaise foi.

Pourquoi as-tu besoin d'étaler ton CV ? Un argument d'autorité ?Voilà qui est, pour le coup, une interprétation (très) abusive. J'indique que j'ai rencontré des personnes qui travaillent sur les sujets évoqués, ce qui ne peut de toute évidence pas être ton cas.

N'empêche que je considére la vérification comme beaucoup plus générale que le testing. Le testing peut être vu comme un cas particulier de la vérification.Bravo : après je ne sais plus combien d'explications, tu persistes encore et toujours. Mais bien sûr, c'est toi qui as raison et les spécialistes de ces domaines qui ont tort.

Quant au reste, même si j'admets que ton attitude bornée consistant à répéter ad nauseam les mêmes assertions toujours aussi fausses est passablement irritante, je te signale que je ne t'ai jamais insulté et t'invite à en faire de même.

1 état ---execution--> 1 état
Ça, c'est un test. Ce qu'on appelle tester, c'est trouver et appliquer un jeu de tests, càd une collection de tests satisfaisant des critères bien définis, notamment de couverture.

Je ne vais pas répéter encore une fois ce que j'ai déjà dit deux fois, j'ai bien compris que tu tiens à faire profiter tout le monde de ton ignorance de ces deux domaines bien distincts et, par ailleurs, fort intéressants tous les deux. J'ai baigné dans les deux milieux quand j'étais moi-même doctorant au LRI. J'y ai travaillé avec les membres de l'équipe parall, entre autres ceux qui font du model-checking. J'y ai aussi rencontré par exemple Marie-Claude Gaudel et des membres de son équipe de génie logiciel, où l'on fait notamment de la recherche sur le test de programmes. J'y ai aussi rencontré des membres de l'équipe de démonstration et programmation, dont entre autres Jean-Christophe Filliâtre, et je serais très étonné, pour employer une litote, qu'il considère ses travaux comme "supérieurs" à ceux de Marie-Claude.

Au passage, puisque tu es tellement plus fort que tous ces incompétents de chercheurs, tu pourrais aller dire au CEA que les recherches sur le test de logiciels de contrôle-commande que l'on y conduit sont inutiles. Ça va sûrement beaucoup les intéresser.

La vérification consiste à construire (ou obtenir) une spécification et prouver qu'un code source s'y conforme. Le test consiste à placer le programme exécutable dans les conditions - à trouver, ce qui n'a rien d'évident - dans lesquelles il est susceptible d'être utilisé et... voir ce qui se produit. Ce sont deux choses différentes, orthogonales, toutes deux indispensables dans un projet où la sûreté est importante.
Je dis simplement que la vérification est supérieure aux testsCeci a à peu près autant de sens qu'affirmer que C++ est supérieur à XML.

Tu dis une chose et son contraire dans le même texte. Avec des méthodes de vérification, on arrive actuellement à prouver un petit nombre de propriétés d'un programme, voire la correction d'un petit programme, mais guère plus. C'est insuffisant dès lors que le programme va être utilisé pour des applications importantes, en particulier si un bug peut avoir des effets désastreux (pas forcément en vies humaines : le bug du Pentium a coûté cher à Intel en relations publiques). C'est aussi insuffisant dès lors que le milieu dans lequel on va utiliser le programme est difficile à simuler.

Prouver un programme ne dispense pas de le tester (souvenir de mon module de tests en M2 : Intel avait une preuve de correction pour l'instruction FDIV du Pentium 1...). Les tests seront toujours là pour ce que les preuves ne peuvent pas prévoir. Évidemment, il y a une énorme marge pour remplacer des tests par des preuves là où c'est approprié.

transmise par des conoisseurs, pas par des journalistes"Les journalistes, c'est comme les... Enfin, y'en a des bien.

Je dirais que la vérification est le propre des scientifiques, dans la mesure ou tout le système de la recherche repose là dessusIl faut vraiment le dire très vite. En théorie, tu as raison. En pratique, il pleut de temps en temps au pays des Bisounours.

sur Ars Technica : http://arstechnica.com/news.ars/post/20090120-ibm-mainframe-(...)

Dans la liste de claviers orthogonaux que tu cites, il y en a
* des (vraiment beaucoup) plus chers que le Typematrix 2030 ;
* des claviers pour enfants ;
* des claviers inconfortables (voir tests).

Donc finalement le 2030 n'est pas si mal...

On peut parfaitement dire ce qu'il ne faut pas faire dans le cadre d'un cours ; il faut en revanche éviter de donner le mauvais exemple, ce qui est différent. En informatique, si on veut dire qu'il faut bien documenter son projet pour que la communication entre les participants se passe bien, on peut utiliser l'exemple du crash de Mars_Climate_Orbiter en n'oubliant pas d'ajouter une couche ensuite sur les bonnes pratiques qui auraient évité la catastrophe. Dans un enseignement plus appliqué (le secourisme dans mon cas), je peux donner à l'oral les conséquences d'une réanimation trop rapide ou trop lente pour que les stagiaires comprennent l'importance d'un bon rythme, mais en tant que moniteur, directement après cette explication, je montre le geste correct (uniquement). Remarque que dans l'article, la plupart des paragraphes finissent de façon constructive : non pas "voici ce qui est mal", mais "voici comment s'améliorer".

Le site de l'ADEME indique comment se procurer des autocollants [1], mais tu peux aussi simplement écrire "pas de publicité" sur ta boîte à lettres, ça marche aussi bien en moins joli (si tu es en France, en tous cas). C'est un bon moyen de sauver des arbres. Alternativement, on peut manger des castors.

[1] http://www2.ademe.fr/servlet/KBaseShow?sort=-1&m=3&c(...)

En effet, il y a une faute : il aurait fallu écrire Le DHCP m'a tuer.

-->[]

oui enfin, ils arrivent après plusieurs annonces le promettant pour l'été 2008, puis la rentrée, puis fin septembre... J'avais jeté mon dévolu dessus, mais j'ai dû aller le ramasser pour finalement acheter autre chose vu que mon départ, lui, n'a pas été repoussé.

Le 900A est disponible depuis quelque temps, notamment dans un magasin qui porte le nom d'un célèbre corsaire. Il a moins d'autonomie que le 901, mais la batterie est plus légère. Il a aussi moins d'espace sur le SSD (8 Go contre 20 Go), mais pour 50€ de moins. Et, surtout, on peut réellement aller dans un magasin et repartir avec, pas (encore) comme le 901.

Et enfin, l'argument définitif : il est vendu uniquement avec Linux :-)

Dans ce cas, je conseille à tous ceux qui se sont rassemblés pour écrire ce message sous la direction d'Ernest de s'y mettre, car il y a plein de choses à trouver dans les livrets accompagnant les albums. Pas seulement ceux de Thiéfaine, je pense aussi à Manset, Burger, Fersen, &c.

Le terme auteur n'est pas limité aux livres, HFT est auteur-compositeur-interprète. Et ses chansons, bien que fort inégales, sont largement plus intéressantes que leur poids de livres hautement dispensables.

D'un côté, oui. Entre les failleurewôles, les eubes et les souitches, on peut avoir l'impression que l'abus d'anglais va de peer en peer.

Et pourtant, sur les blogues et les sites les plus "sérieux" en particulier, les efforts sont visibles. Tout récemment, j'ai vu le pavé tactile remplacer le teutchepade, le jeu de composants régler son compte au tchipsette, le canal supplanter le channel, etc. Alors certes, on trouvera certainement encore longtemps des clavardoirs consacrés aux netbooks dual core fanless, mais tout de même, il ne faut pas désespérer.

- messieurs & mesdames -> et

Qu'as-tu contre l'esperluette ? Nonobstant ce qu'en dit l'article de Wikipédia que je viens pourtant de citer, l'ex-27e lettre de notre alphabet est toujours utilisée par certains auteurs contemporains, par exemple Hubert-Félix Thiéfaine.

Personnellement je me suis dit que le journal méritait de passer en dépêche.Avec un texte un peu plus étoffé, ça se regarde. Mais il reste un problème : il n'y a ni vidéo sous-titrée en français, ni transcription en français. Que les volontaires se signalent...

Disons que les sujet "rip" etc... y'en a un peu marre...
1. Sur la page d'accueil des journaux, je n'en vois qu'un (celui sur les Rroms en Italie).
2. Tu aurais pu le dire clairement et un seul commentaire aurait suffi.
3. Il est normal que l'on traite souvent la mort d'une personne dans l'actualité, c'est l'occasion de revenir sur ce qu'elle a apporté.
4. Randy a justement été fortement médiatisé lorsqu'il a annoncé son cancer et sa mort prochaine.

Le pire dans ce journal, c'est que l'auteur n'a aucun mots réconfortant pour la famille
Randy ne voulait pas que l'on parle de sa mort dans le style larmoyant habituel. Il voulait qu'on se souvienne de son œuvre, des conseils qu'il a donnés, et il s'est occupé tout seul de préparer sa famille. Tu saurais tout ça si tu avais regardé la vidéo et/ou lu la transcription.

Je le conseille chaudement : depuis que j'y suis, j'ai découvert le concept révolutionnaire de banquiers qui ont autre chose en tête que tirer à tout prix le maximum d'argent de leurs clients. C'est vraiment agréable de se voir proposer les produits qui conviennent le mieux à sa situation plutôt que ceux qui rapportent la plus grosse commission au vendeur (vécu avec ma banque précédente, une Banque Populaire : comme quoi, l'appartenance à un même groupe ne signifie pas grand-chose). Le côté éthique est représenté par des moyens de paiement (carte Agir) et d'épargne qui, en gros, soit donnent lieu à un don de temps en temps à une association, soit servent à financer des micro-crédits. Quant au site web, il me suffit pour ne pas avoir besoin d'aller au guichet, sachant que je suis sous Linux avec Firefox.

Chez nous (Paris Sud), ça fait partie du cursus de base du master 2 recherche. Du reste, les prérequis sont assez costauds : théorie des automates, logique temporelle, probabilités (chaînes de Markov et compagnie)... Le domaine gagnerait à être mieux connu car c'est l'un de ceux où la recherche et l'industrie s'accordent à penser qu'il y a beaucoup à faire.

Des étudiants m'ont fait le coup ici même, en France. Avec une variante : pour une source en anglais, la traduction automatique. C'est dire à quel point c'est discret...