outs a écrit 292 commentaires

n'oublie pas \usepackage{lmodern} sinon les polices sont moches

c'est bien le cas sur HL2, on peut le changer à la volée. Ce que je suis obligé de faire pour éviter les nausées...

Mon nom de fichier le plus long est probablement «2004 - Beauquier, Crolard, Prokofieva - Automatic Parametric Verification of a Root Contention Protocol Based on Abstract State Machines and First Order Timed Logic.pdf»

C'est un article scientifique, j'ai longtemps hésité pour ma convention de nommage, mais le plus simple c'est encore de tout noter (date, auteurs, titre) (et en utilisant des espaces). Et cela peut être long.

Alors effectivement utiliser des métadonnés serait mieux, et d'ailleurs j'ai quelques fichiers pdf ou la métadonnée titre est bien saisie mais c'est rare. Ça arrive notamment quand l'auteur a utilisé le package latex hyperref, mais cela reste rare même si on regarde les pdf «officiels» des éditeurs.

Sinon le système de gestion des métadonnés sous linux avance doucement, il faut regarder du coté de en:NEPOMUK_(framework) notamment. Mais c'est pas encore super au point.

ça évite d'avoir à gérer des troupeau de pingouin !

N'est-ce pas trop compliqué pour des débutants ?
Perso, je dirai non mais a condition ne pas forcer à mettre des catch ni a déclarer que l'on peut en envoyer (en gros pas comme en java)

C'est gentil mais on connais déjà. Évidement il y a beaucoup d'information, le problème justement c'est qu'il y en a trop. Genre le wiki recense toutes les distribs qui existent, alors oui c'est cool mais jusqu'ici je n'ai pas eu le temps de toutes les essayer pour les comparer sans compter qu'il faut a chaque fois bidouiller et appliquer des patchs pour régler les bug.

C'est pour cela que je demandais simplement dans quelle direction aller... (sachant que pour le moment je veux juste téléphoner). J'ai eu des résultats pas trop mal avec la distrib basée sur qt sauf des problème de son trop faible. Du coup impossible de téléphoner dans les transports, ce qui est bloquant pour moi. Le bug est connu, il est dans le tracker de nokia... et cette distrib est donnée comme la meilleur si on veut simplement téléphoner.
Enfin bref, ca coute rien au mec de nous dire laquelle il a pris en tout cas ...

Quel système a tu installé ? Le problème aussi c'est de choisir entre les 7 distributions qui existent ...

Apple a une flopée de brevet sur l'interface multi-touch et compte surement attaquer quiconque proposera cette fonction ...

Non mais n'importe quoi :)
1) on n'observe pas les contre-exemple et 2) on ne prouve pas les cygnes...

Les cygnes font partit du monde réel, donc si on a une théorie (tous les cygnes sont blanc) on fait des expériences et des observations pour la vérifier (exemple: biologie, physique)

Maintenant si on en science hypothéco-déductive (mathématique, informatique) on pose des définitions (on appelle un cygne un oiseau aquatique de couleur blanche) et après on en déduit des propriétés avec des démonstrations et des contre-exemple.

Mais on mélange pas tout :)

De plus on peut manipuler des raisonnements à l'infini, ce n'est pas un problème.

Et pour les tests on cite toujours Dijkstra d'habitude:
"Program testing can be used to show the presence of bugs, but never to show their absence!"
http://en.wikiquote.org/wiki/Edsger_W._Dijkstra

Dans la pratique les processeurs grand public sont bourré de caches prédictif et de pipeline ce qui rend la détermination du temps d'exécution au pire des cas très pessimiste par rapport au cas moyen.
De plus effectivement les OS normaux n'ont pas de garantie de schéduling temps-réel. D'ailleur linux sans patch n'est pas très bon a ce jeu là.

Après effectivement en théorique tu peut quand même faire une analyse formelle des prop temps-réel mais elle sera très pessimiste pour être utilisable en pratique (c'est a dire qu'on sous utilisera la puissance du processeur). Mais en pratique on met des logiciels temps-réel sur les OS et du matos adapté donc y'a pas trop lieu de polémiquer sans fin.

Ben ce qui est du temps réel mou (soft realtime) ben par définition c'est pas grave si on loupe des deadline, donc l'intéret de faire une preuve formelle est moins évidente.

Oué bah on en revient toujours à la base : en dehors des domaines où la sécurité est primordiale, en général personne se fait chier à atteindre le niveau de spécification formelle nécessaire à l'utilisation de ces méthodes de vérification.

On peut trouver des compromis, des lightweight formal method, par exemple on fait des modèles formel mais pas exhaustif et on s'en sert pour générer des jeux de test. Après on peut en rester là ou aller plus loin dans la preuve sur le modèle si il y a un intéret/budget.
Il y a pas mal de projet comme çà, c'est intéressant je pense.

Bon, sinon, je vois plusieurs réflexions sur le fait que la preuve d'un programme ne peut être fait de manière générale, et alors ? Du moment qu'elle le fait au moins aussi bien que le ferait un humain et en plus rapide, ça vaut le coups non ?

En pratique ce n'est pas le cas, on passe beaucoup de temps à s'arracher les cheveux pour comprendre pourquoi le prouveur automatique n'ai pas capable de faire ce truc qui a l'air trivial...

Après oui effectivement il y a des techniques «pousse-bouton» qui ne font que chercher a trouver des bug sans chercher l'exhaustivité et cela peut faire gagner pas mal de temps. Mais cela nécessite quand même d'écrire une spécification formelle et c'est souvent la dessus que les gens ont du mal.

En passant le logiciel pour faire de la méthode B évènementielle, développé lors du projet de recherche européen Rodin (c'est aussi le nom du logiciel), est un logiciel libre :
http://sourceforge.net/projects/rodin-b-sharp/
il y a un prouveur dedans qui est libre aussi, par contre ceux qu'on installe avec le plugin proviennent de l'atelierB de clearsy ( http://www.clearsy.com/ )

Ben en fait dans l'ingénierie classique les méthodes formelles sont déjà la norme suffit de remplacer le terme «méthode formelle» par «résistance des matériaux» ou «thermodynamique» etc...
Par exemple quand on construit un pont, on sait déjà (avant de le construire) que le pont va résister si on met des camions de 33t dessus, cela n'empêche pas d'essayer effectivement de mettre des camions dessus quand on a fini de le construire, comme tu l'à fait remarqué.

Après le problème de l'informatique c'est qu'actuellement on ne fournit pas (usuellement) de garantie sur la qualité des logiciels. Si les freins de ma voiture lâchent, je peux attaquer le constructeur de la voiture. Mais si un logiciel m'a fait perdre ma compta la clause de non-responsabilité du fournisseur de logiciel empêche de demander de réparations.

De plus il faut bien distinguer deux types de tests : les tests type unitaires et les tests d'intégrations. Je t'assure que la preuve formelle fournit une garantie bien plus forte que que les tests unitaires sur l'absence de bug. Mais même avec des preuves formelles il faut toujours faire des tests d'intégration car il faut *valider* la spécification formelle. C'est à dire est ce que c'est la bonne spec ? et est-ce qu'on a pas oublié des propriétés importantes ? La preuve ne fait que *vérifier* la spec, des propriétés ou le code produit

ah oui effectivement c'est bien. Merci. (comment j'ai pu passer a coté dans mes recherches ?...)

en fait il y a trois projet avec +/- le même nom qui font cela :
* http://pdfcrop.sourceforge.net/
* http://code.google.com/p/pdfcrop2/
* http://www.ctan.org/tex-archive/support/pdfcrop/

non...
mais bien essayé :)

Bha si je veux aller de Metz à Lyon le plus rapide c'est de passer par Paris en TGV alors ...

Et de tout manière avec la sncf «tout est possible»

Ce n'est pas un argument ça. Ce n'est pas parcequ'on paye qu'on possède quelque chose...

en fait cette option apparait avec le profile «advanced» dans Éditions>préférences
C'est ptet pour ça que tu ne la vois pas

FIchier>nouveau dessin (ctrl n g)

les outils de dessins sont basiques.

par contre on peut mettre des formules de math mathml dans le svg. Ca c'est pas courant.

Ben oui ! En plus dans la poche c'est super pratique :)

Merci pour ce test qui m'a appris plusieurs petites choses, étant nouvel utilisateur de Fedora.

Quelques remarques en passant :
* "projet Fedora dans sa dixième incantation"
on incante des distrib maintenant ? :) heureusement qu'on ne les décante pas encore !

* "Cette nouvelle version compote"
de pomme ? :)

* "Vous pouvez donc installer le RPM de configuration de Fusion (marche également pour Fedora 8 et 9). Vous pourrez alors installer les paquets dont vous avez besoin tels que Flash et la lecture de DVDs."
Flash ne fait pas partit de ce repo, il est dans celui d'adobe.

Le eeetop alors :
http://www.blogeee.net/2008/10/10/eeetop-caracteristiques-et(...)
mais ca reste à 500€

Je pense que tu peux ajouter seulement les lignes de conf qui t'intéresse. xorg utilisera l'autodetection pour les lignes manquantes.

On algo on m'a appris à faire l'analyse des performances au pire des cas. Apparemment chez les économistes c'est plutôt le contraire :)

Perso j'aurai tendance à douter des mecs qui pensent que des système avec des croissances perpétuelle existent.