Nicolas Boulay a écrit 16010 commentaires

J'ai du me tromper alors. Je parles évidement de la taille de ce que fournis l'humain pour faire la preuve.

Ensuite, il faut aussi prouver le prouver, ce qui n'est pas gagné.

"La première sécurité est la liberté"

Ma question était de savoir si il existait d'autres méthodes.

J'imagine que écrire le code puis écrire sa preuve devrait aussi suffire.

Mais d'après les exemples de "Why" pour un code de 20 lignes, il y en a 1000 de preuves. On est loin d'être utilisable.

"La première sécurité est la liberté"

Si la propriété est une spécification (totale) alors spec est déjà en quelque sorte le programme en lui-même. Si cette spec était "exécutée", par une machine, son comportement serait le même que celui du programme à vérifier.

Je comprends bien. D'où la recherche de l'écriture de spec exécutable (est ce que tu connais Scade ? c'est l'argument des LLR executable pour le vendre).

Mais il existe toujours un moment il faut spécifier ce que tu mets dans la spec. Il y a toujours une spec de spec en cascade.

Donc, il y a toujours à un moment l'écriture de quelques choses de non ambigüe et l'écriture du code final. Ce qui revient à avoir 2 "modèles", non ?

"La première sécurité est la liberté"

tu travaillais ou avec Esterel ? Chez TI ?

"La première sécurité est la liberté"

Cela revient à écrire 2 fois le même programme dans des paradigmes différents et de vérifier qu'ils produisent les mêmes résultats...

Mais lors d'une recherche de meilleur qualité, il n'y a pas d'autres solutions non ?

"La première sécurité est la liberté"

Tu parles quand même dans un cadre très général bien loin des cas pratiques.

- de déterminer si ce programme fait la même chose qu'un autre programme

Dans le cas général.

Parce que c'est justement dans ce domaine là que les prouveurs formelles sont utilisés industriellement à grande échelle. On appelle cela les "equivalence checker". C'est un outil du domaine de l'EDA qui permet de s'assurer qu'une mer de portes générées par un synthétiseur est équivalent au code source HDL.

- et par extension de déterminer si ce programme est conforme à sa spécification

Il faut encore savoir ce qu'est une spec. Souvent, c'est super flou et pas clair. Le client veut que le produit réponde à son problème et ne plante pas, par contre, il ne sait pas forcément bien le définir. C'est plus un problème d'ingénierie logiciel que de preuves mathématiques.

"La première sécurité est la liberté"

Tu pourrais nous expliquer le genre de code qui est fournis à un assistant de preuve, par exemple, en utilisant du pseudo code ?

Dans le milieu de l'aéronautique, il est souvent question de comparaison de modèles et de confrontation d'interprétation de spec entre 2 équipes utilisant des outils différents. Donc, on a une équipe qui développe le programme et l'autre un modèle sous une autre forme. On compare ensuite les résultats de tests définit par avance par l'équipe de test (mais qui pourrait être généré automatiquement par classe d'équivalence des entrées et couverture de code)

Le but serait ici de facilité la vie de la deuxième équipe.

"La première sécurité est la liberté"

D'ailleurs, y'a ESL Technology qui est à racheter (ex-Esterel EDA), la boite qui a repris le langage Esterel. 10 ans de R&D. Elle est en faillite suite à l'arrêt de la moitié des contrats de prestation du principale client TI.

L'intégration de le preuve est assez sympa. Le langage lui-même fait passer le VHDL pour de l'assembleur par rapport à Java.

"La première sécurité est la liberté"

Dans ce cas là, c'est l'outil qui l'a fait à ta place /o\

"La première sécurité est la liberté"

Ce que tu dis, c'est justement que c'est très précieux, car cela trouve jusqu'au manquement de la spec. Cela repousse le travail idiot du test systématique par une recherche d'une meilleur cohérence de spec et d'un test de haut niveau.

Personne n'a jamais dit qu'un ordinateur ferait tout le boulot à ta place.

Sinon dans les prouveurs "100% automatique", il recherche si il existe les conditions de plantage du code C, comme les "array out of bound", les division par zéro. Le but est ici de prouver que le code ne plante pas, pas qu'il correspond à la spec. C'est déjà pas mal car on ne demande rien aux codeurs "en plus".

D'une manière général, la preuve, c'est génial, sauf que cela passe rarement à l'échelle (pb numero 1) et "les gens" ne font pas confiance à un "toujours vrai" rendu par un outil, par contre, ils aiment bien qu'on trouve leur bug.

"La première sécurité est la liberté"

Vu que DirectFB ne sait que gérer des "layers", cela n'a pas franchement d'intérêt sauf si il sait aussi gérer le reste de l'interface.

"La première sécurité est la liberté"

En fait exFAt, est plus proche de EXT3/EXT4 que de FAT32 :/

"La première sécurité est la liberté"

Ce qui veut dire que vu la politique d'agressions choisit par Microsoft il sera impossible de lire des cartes de ce style sur les OS libres.

Ce qui veut dire qu'il sera refusé.
Dans ce cas, le plus rapide serait un ext2 light, sans permission. Cela ne devrait pas être trop dure à écrire.

"La première sécurité est la liberté"

Ou alors c'est une pression pour racheter TomTom. Pas impossible non plus.

Et ensuite, faire en sorte que Tomtom perde le procès pour faire jurisprudence en leur faveur ?

"La première sécurité est la liberté"

Tu voudrais une version light de ext2 ou de ext3 ?

Dans ce cas, il ne faudrait pas mieux quelques choses de dédié comme logfs ou autre système pour le stockage lent ?

"La première sécurité est la liberté"

DirectFB est une interface simpliste à tous les hardware du marché qui n'utilise quasiment rien de haut niveau (accélération hw).

Le but c'est d'être simple et de marcher partout, si tu veux du plus haut niveau attaque en openGL.

"La première sécurité est la liberté"

ben non, c'est pour en faire un swap.

"La première sécurité est la liberté"

Depuis la 3.0, ce n'est plus vrai.

"La première sécurité est la liberté"

Les défauts que tu cites sont du niveau de l'arrachage de prise sans sauvegarde automatique.

En te lisant, on se dit que le problème est plutôt entre la chaise et le clavier, ton but avec cette expérience n'est pas d'essayer la Mandriva mais de lui casser du sucre sur le dos pour dire "***" c'est mieux.

"La première sécurité est la liberté"

Les LCDs qui ont des contrastes de fou jouent aussi sur l'éclairage arrière.

Les plasma doivent être encore plus sensible à cet effet.

"La première sécurité est la liberté"

Je commence à voir où je me plante. Merci.

"La première sécurité est la liberté"

Disons qu'aujourd'hui, un GPU est surtout capable de faire un nombre de MAC 10x supérieur à un CPU si il n'y a pas trop de dépendance de donné et si tu n'exploses pas le nombre de registre interne. C'est donc assez limitant.

"La première sécurité est la liberté"

de toute façon en général les autres (État, banques, etc.) se servent avant lors de la liquidation

ça, c'est lamentable. Vu la fragilité de leur finance, les PME devrait être servi en premier mais j'imagine qu'il doit exister des moyens de faillites frauduleuse pour ne pas payer le fisc :/

"La première sécurité est la liberté"

Or il est quelconque. C'est "programme" qui défini son comportement vis-à-vis de la donnée, qu'il peut très bien considérer comme une fonction avec des arguments si il a envie.

Mais dans ce cas, tu retombes dans le problème de la string infinie (pour le cas du programme qui prend en paramètre un programme et qui s'avale lui-même, au hasard halt()).

Et si tu rajoutes les données dans ta 2ième string, dans halt(halt1,halt2) halt2 ne contient pas de donné à sa suite, il contient donc "null" ?

"La première sécurité est la liberté"

Je suis microelectronicien, je sais à quoi ressemble un code objet (binaire)...

Tu oublis le cas du compilo C de l'interpréteur python qui exécute un script.

C'est pas en connaissant le compilo C et le code C de l'interpréteur que tu peux conclure quoi que ce soit sur le script.

"La première sécurité est la liberté"