David Mentré a écrit 31 commentaires

Bonjour,

Pourquoi un nouvel analyseur a été développé au lieu d'utiliser Frama-C/Value Analysis ?

Quels intérêts et différences principales d'IKOS par rapport à Frama-C/Value Analysis au jour d'aujourd'hui ?

Merci,
david

Non, nous n'avons pas prévu d'enregistrer la conf.

Correction : je ne voyais pas les avatars et avec le certificat ça va mieux. :-)

Si tu n'aimes pas les langages qui te trouvent les bugs à la compilation, c'est que tu n'as pas fait assez de programmation. ;-) En plus de l'Ada, tu devrais tester OCaml ou Haskell.

L'Ada est largement utilisé pour les logiciels critiques dans le domaine ferroviaire (logiciels à bord des TGV, contrôle des trains au sols, métros automatiques), aéronautique ou spatial (Ariane).

Moi aussi j'aime bien l'Ada et je regrette qu'il soit autant délaissé, à tord à mon avis.

Je confirme, « l’inspection de code formel » de McConnell n'a rien à voir avec les analyses statiques et notamment les méthodes formelles. Le « formel » dans l'inspection de code, c'est qu'on suit une procédure codifiée.

Côté analyses statiques, on distingue les approches non formelles, les bug finders et les approches formelles comme Astrée, Frama-C, la Méthode B, SPARK, etc. Les deux sont utiles, les bug finders sont plus facile à utiliser mais pouvant donner des faux positifs ou des faux négatifs. Les approches formelles donnent des garanties plus fortes (si pas d'alarme alors le logiciel est garanti sans un certain type de fautes) mais sont plus difficiles à utiliser (mais largement utilisables pour certains).

Pour ceux que ça intéresse, je maintiens une liste de tous les outils libres formels. Il y a de tout, de logiciels ultra spécialisés à des environnements de développement et preuve pour une approche particulière : gulliver.eu.org/free_software_for_formal_verification.

PS : Je ne vois pas le graphe, pourtant j'ai installé le certificat. Je vois bien les avatars.

Très bonne dépêche ! j'ai beau suivre la caml-list, je reste un utilisateur me contentant du noyau historique. Cette introduction aux nouvelles fonctionnalités est vraiment bien faite et pédagogique. Merci !

A part la ligne 14, ils l'ont utilisé ailleurs ?

:-) Pas mal oui : http://www.clearsy.com/wp-content/uploads/carte-monde-b-fr.jpg

Le KVB qui contrôle la vitesse des TGV est développé en B. Des gestions d'aiguillages d'Alstom sont développés en B. etc.

Le ferroviaire aime bien le formel avec des produits de http://www.absint.com/ . Mais ils s'agit souvent de prouver "des théorèmes" et non des "spec complètes".

Tu peux jeter un œil sur le travail fait par ClearSy pour le CBTC de Thales sur la Flushing Line de New York. Le but est bien de prouver des propriétés système (i.e. dans une spec complète).
http://www.tools.clearsy.com/resources/formal-proofs-for-the-nyct-line-7-modernization-project/

Dans l'aéronautique, ils n'aiment pas trop.

Assertion un peu gratuite. Le standard DO-178C permet justement d'utiliser des méthodes formelles pour remplacer des tests, ce que la version précédente (178B) ne permettait pas. Et il y a aussi le DO-333 ("Formal Methods Supplement to DO-178C and DO-278A").

Airbus est un gros consommateur de méthodes et outils formels : CAVEAT, FLUCTUAT, Astrée, SCADE, CompCert, Frama-C, …

Par ailleurs il semblerait que les preuves faites sur le protocole TLS ne couvrent pas tous les cas possibles ; je
conseille l'article suivant, qui est très intéressant (une vulnérabilité trouvée récemment dans le protocole lui-même) :
http://blog.cryptographyengineering.com/2014/04/attack-of-week-triple-handshakes-3shake.html

Ben en fait, cette faille a été découverte par des gens qui veulent prouver formellement TLS : miTLS (http://www.mitls.org/) écrit en F# et spécifié en F7.

Le code des participants est mis en libre mais le code du site et tous les exemples sont propriétaires. C'est pas un peu abuser ?

http://www.codingame.com/cg/#!page:terms

« L’ensemble des éléments figurant sur ce site sont protégés par les dispositions du Code de la Propriété Intellectuelle. En conséquence, toute reproduction de ceux-ci, totale ou partielle, ou imitation, sans notre accord exprès, préalable et écrit, est interdite. »

Salut,

> - taille de la BD importée depuis OSM

Environ 70 Go. Le daily diff importé quotidiennement fait environ 30-60 Mo compressé.

> - temps pour générer une carte (préciser le hardware)

Quelques minutes pour les grosses villes (4 min pour Cambridge par exemple : [http://maposmatic.org/jobs/6030]).

Machine avec 2 Go de RAM, un dual core E2180 @ 2.00GHz.

> - nombre de cartes générées par jour

Il faut attendre un peu que ça se stabilise. Depuis septembre, on a fait environ 6000 demandes soit 30 demandes par jour.

Amicalement,
david

par contre ça ne marche pas toujours. Par exemple ça marche avec la RFC de HTTP (#2616), mais pas avec la text/enriched MIME Content-type (#1896).

Le format des RFC n'est pas entièrement figé et varie d'une RFC à l'autre. Les regexp utilisées pour identifier les éléments sont plutôt du genre « ça marche bien en général » que « le fonctionnement est garanti », et bien souvent améliorer un cas particulier dégrade un autre cas.

Mais vous pouvez toujours renvoyer un rapport de bug avec des exemples précis (telle RFC à tel endroit) à l'auteur, on verra si on peut améliorer la chose.

Amicalement,
d.

il y a pas besoin d'un truc particulier pour lire ce genre de doc

Bien évidemment, il n'y a pas besoin de qRFCview pour lire du texte. Mais l'ajout d'une table des matières ou d'un renvoi à une section est très pratique quand on lit une RFC un tant soit peu compliquée, où les renvois sont très fréquents.

Amicalement,
d.

Toutefois, comme le soulignent les commentaires sur Linux Weekly News, tout contributeur à OpenOffice.org doit signer un accord qui prévoit que les contributions deviennent la propriété commune de Sun et du contributeur. Sun peut donc les utiliser à loisir dans son produit propriétaire StarOffice.

Bon, on peut trouver ça pas génial d'être obliger de contribuer à un logiciel propriétaire (StarOffice) si on veut contribuer à un logiciel libre (OOo). Mais d'un autre côté, on peut considérer ça comme une juste rétribution de Sun. 10 millions de lignes de code, ce n'est pas rien quand même !

J'avais trouvé ça juste à l'époque de Mozilla et sa licence MPL, je continue de trouver ça juste aujourd'hui pour OOo.

d.

Pour la rapitdité de dev, je pense plus à perl qu'à ocaml :)

J'ai découvert OCaml en 2e année de thèse. A l'époque, je faisais un logiciel de traitement symbolique et je l'avais commencé en Perl. Au-delà de 1.000 lignes, Perl est une vraie daube(tm) : un cauchemar pour faire de la programmation claire (le moto : "y'a toujours un comportement par défaut" de Perl devient très vite ingérable. Le programme tourne mais ne fait jamais ce que l'on veut).

J'ai commencé OCaml en lisant le bouquin de Leroy et Weis sur la plage, pendant mes vacances. En revenant, j'ai codé direct la nouvelle version : depuis, je suis un fan d'OCaml. Je trouve que mon code est clair, bien structuré et efficace. Et tu limites pas mal de bug par construction.

Evidemment, pour un petit script de vérif de sortie de brochage d'un FPGA par rapport à un logiciel de CAO, je sort mon Perl. Mais dès que je veux faire un programme, c'est à dire quelque chose de structuré qui doit durer, je ne vois pas mieux qu'OCaml (suivant les cas, cf. mon exposé).

Vu le niveau d'abstraction, le compilo d'ocaml pourrait faire des choses impossible ou difficile en C comme le controle du layout mémoire ou l'utilisation du SIMD.

Si je me souviens bien, OCaml fait quelques siouxeries sur IA64. Quand au contrôle du layout mémoire, c'est LE point sur lequel je voudrais qu'OCaml progresse. Mais j'ai pas encore les idées claires sur ce qu'il faudrait faire.

Pourquoi Ocaml est encore derrière le C en terme de vitesse ?

Parce que les développeurs d'OCaml ne cherchent pas à faire les super-optimisations de scheduling d'instruction qui permettraient de gratter les quelques cycles manquants en calcul numérique pur.

Parce que OCaml a quand même un ramasse miettes, et qu'il a un surcoût (léger certes, mais surcoût quand même).

Parce qu'un processeur est conçu pour exécuter du C et pas du OCaml. Mais ça ça changera quand on fera nos processeurs libres. ;-)

J'entend aussi beaucoup de bien d'Haskell. Quelqu'un connais les + et les - des deux. Je crois que ce sont tous les deux des enfants de ML ?

Haskell fait du fonctionnel pure. C'est très séduisant car on peut raisonner sur les programmes. En pratique, Haskell est plus lent qu'OCaml, mais pas au point que ce soit inutilisable. Au niveau langage, chacun des deux a ses spécificités, après c'est à chaque programmeur de dire ce qu'il préfère.

Qu'est ce qui motive l'INRIA dans OCaml ?

Tu veux dire : qu'est qui motive les développeurs d'OCaml à continuer ? Ben c'est leur bébé. Et ces derniers temps, ça va plutôt bien pour OCaml. Evidemment, sur 30 ans, on ne sait pas si le langage sera toujours là. Mais dans 30 ans, fera-t-on toujours du Java ou du C ? (pour le C oui, vu le passif... :-)

Pour le calcul scientifique (et donc numérique), un livre complet a été écrit sur le sujet :
http://www.ffconsultancy.com/products/ocaml_for_scientists/(...)

Sinon, son auteur a fait un email récent comparant OCaml à C++ sur x86 32 et 64 bits. OCaml n'est pas toujours le premier mais pas non plus le dernier. Et ne pas oublier qu'il n'y a pas de mémoire à gérer ! Rien que pour ça...

http://caml.inria.fr/pub/ml-archives/caml-list/2005/03/9aa5c15129d1(...)

Et hop ! Sources OOo, HTML et PDF :
http://www.linux-france.org/~dmentre/gulliver/expose-ocaml-2005-04-(...)

Pour ma part, je suis entièrement d'accord avec toi : la plupart du temps, que ce soit pour du proprio ou du libre, on développe toujours comme on faisait du soft dans les années 70. Il faut absolument que les développeurs de logiciel libre s'efforcent de faire un soft sans bugs, avec toutes les techniques possibles.

Par exemple, pour demexp, on utilise :
- un langage de haut niveau, OCaml, avec des fonctionnalités qui évitent certaines classes de bug (un garbage collector pour les bugs mémoires, l'inférence de type pour les bugs sur les structures de données, des exceptions pour les cas d'erreur, ...) ;

- un code documenté avec de la programmation littéraire (voir par exemple http://www.linux-france.org/~dmentre/demexp/demexp-server-book-2005(...) ) ;

- utilisation de générateurs de code à partir de description déclaratives dès que c'est possible. Par exemple la description XDR des formats de messages réseaux nous permet de générer automatiquement les routines d'encodage/décodage ;

- des tests unitaires systématiques pour chaque module, y compris les cas d'erreur. Les tests sont remis à jour quand le code bouge ;

- des tests d'intégration. Comme demexp est un client serveur, le serveur a un mode --autotests où une thread cliente est créée, elle se connecte au serveur et effectue toutes les actions attendues d'un client (y compris tester les cas d'erreur).

J'ai pas encore eu le temps de faire de la vérification formelle, mais j'y pense.

Evidemment, il y a toujours des bugs. Mais au moins les dégâts sont limités.

Bien que fournit avec le source et modifiable par l'utilisateur, Squeak n'est pas un logiciel libre, ni au sens d'OpenSource, ni au sens de la Debian DFSG.

Pour plus de détails : http://minnow.cc.gatech.edu/squeak/159(...)

C'est quoi l'interet de faire un doublon avec Lyx?

Ce n'est pas du tout la même philosophie. LyX est juste une interface graphique à LaTeX.

TeXmacs est un éditeur structuré : les documents sont hiérarchisés et l'éditeur a connaissance de cette structure. Si on fait une recherche dans une matrice, la recherche ne déborde pas en dehors de la matrice.

Un autre gros avantage de TeXmacs, c'est qu'il peut servir d'interface à de nombreux systèmes de calculs mathématiques, libres ou non, symboliques ou non.

Tout le crédit est à attribuer en fait à Bobert, auteur d'une niouze sur une précédente version de TeXmacs d'où nous avons repompé le descriptif qui manquait un peu dans celle ci. La petite touche trollesque y était tellement savoureuse qu'il aurait été vraiment grossier de la retirer.

Mouais. En tant qu'auteur de la news, j'apprécie pas trop ce genre de bidouille. C'est très loin des simples corrections orthographiques, ce genre de modifs !

Si vous n'étiez pas content du contenu de la news, et bien il fallait la refuser et me demander de la retravailler. C'est quand même mon nom qui est en haut de la news. Ou alors vous auriez du marquer clairement les parties ajoutées avec une NdM.

Groupf!! (pas content)

L'idée principale n'est pas de faire du Prolog mais d'intégrer dans Axiom un système de vérification formel pour prouver des parties de l'Algèbre. Une très très vaste tache. Un candidat est ACL2 (il repose sur le même Gnu Common Lisp qu'Axiom) : http://www.cs.utexas.edu/users/moore/acl2/(...)

Amicalement,
d.

Qu'est-ce qui ne marche pas avec le make ?

Amicalement,
d.

<on dévie>
Même au FN !?!! Arghh!!

Ton initiative est très bonne, mais de grâce, pas le Front National ! Ce parti est ouvertement raciste et xénophobe.
</on dévie>