outs a écrit 297 commentaires

La méthode B fait tout ca très bien.

On commence par un modèle abstrait général qui pose le but a atteindre.
On prouve qu'il est cohérent
On écrit un modèle qui raffine le premier en rajouter des detail, par exemple la forme générale de l'implémentation.
On prouve qu'il raffine le premier modèle, c'est à dire qu'il fait la même chose. On prouve qu'il est cohérent.
Et ansi de suite jusqu'a obtenir un modèle avec la precision souhaitée.

Si on le souhaite on peut aller jusqu'a la précision requise pour une implémentation. Dans ce cas on peut générer le code automatiquement. Le code est assez crade en effet, mais ce n'est pas très grave vu qu'il est correcte par contruction pas besoin de le débugger.

Mais il ne faut pas réver, trouver une preuve est un problème indécidable. Il y a un prouveur dans les outils qui arrive faire les plus faciles mais il faut faire les plus complexes à la main. Au final il faut s'accrocher et le temps pour faire tout cela est long mais on arrive a un logiciel 100% certifié.

Pour info cette méthode a déjà été utilisée dans l'industrie, par exemple pour réaliser le logiciel qui pilote le metro parisien METEOR

<<Non, en fait il s'agirait de générer, pour un algorithme, à partir de ses contrats, une preuve en B que l'algo respecte les contrats.>>

Mmmh infaisable.

Enfin générer le modèle B à partir du code et des contrats associé ce n'est pas un probleme : le B étant très expressif.

Mais tu va te retrouver avec un modèle beaucoup trop compliqué et qui n'utilise pas le raffinement. Le prouveur automatique n'aura aucune chance de trouver les preuves.

Hors l'interet principal de B est de distribuer la complexité des preuves en créant plusieurs modèle qui se raffinent les un les autres. Mais écrire ces raffinement demande une réflexion humaine. Pas possible de la faire faire par le compilo.

Plus généralement ca fait depuis 1960-70 qu'il existe des méthodes pour certifier les programmes. Hors cela n'a pas révolutionné l'informatique. Pourquoi ? car tous ces problèmes sont indécidables. Dans certain (model checking) on peut se ramener a un problème NP-complet, mais on est quand même coincé par la complexitée du travail. Il ne faut pas s'attaquer a ca avec naiveté, sans vouloir te vexer.

(4) l'exemple avec la taille est possible dans tous les langage objet, surtout si il y a les template, ce que tu appelle les type paramétrés. C'est donc supporté par Lissac qui est objet à prototype. Ca se passe pas de la même façon mais la puissance de ce mécanisme dans Ocaml provient du mécanismes des types abstrait associé au mécanisme d'inférence.

L'inférence de type c'est une autre paire de manche. Écrire un moteur d'inférence est très complexe et pose des problèmes dans le cadre des langages objet, bien que cela soit dans une certaine mesure possible (cf implémentation objet de Ocaml). Initialement l'inférience est basé sur le typage automatique des lambda-calcul (fondement de la prog fonctionnelle), comme Lissac est objet et non pas fonctionnel il faut réétudier l'inférience dans ce cas.

(5) Le pattern matching est en fait une application des concepts de réécriture. Très souvent ajouté dans les langagues fonctionnels pour les enrichir. Le problème est qu'en objet on doit utiliser le polymorphisme pour éviter les switch entre les cas. Les branchement par cas sont à éviter en prog objet pour améliorer la capacitée du code à évoluer (pas besoin de modifier les switch suffit d'hériter une classe à la place). Il y a clairement un clash entre les deux paradigmes. Cela dit il y a peut être matière à creuser. Demande à ontologia il adore spéculer :))

A noter que l'héritage de code (sous le nom de non-conforming inheritance) à été rajouté dans SmartEiffel version 2.

On peut donc utiliser les même méchanismes maintenant en Eiffel, bien que ce ne soit pas l'habitude.

(et aussi dans le pseudo standard ECMA de Eiffel qui est sortit il n'y a pas très longtemps)

Ce n'est pas comme cela que cela marche.

Il y a bien une table de liaison dynamique avec SmartEiffel. Mais elle est restreinte aux seul cas possibles par l'analyse du code.

Si jamais le compilo trouve qu'il n'y a qu'un seul cas possible il supprime le mécanisme et on se retrouve avec une methode aussi efficace quand dans le cas d'un fonction non virtuel en C++. Avec en différence que l'optimisation est réalisée par le compilateur systématiquement.

Ca c'est pour l'héritage simple. Pour l'héritage multiple c'est encore mieux que cela. Il n'est en effet pas possible d'utiliser dans tous les cas une table pour résoudre le polymorphisme dans le cas multiple, en particulier si il y a des cycles dans les parents de la classes. Dans ce cas il faudrait faire un parcour du graphe. Solution très couteuse (c'est une des raisons pour laquelle pas mal de langague ne supportent pas l'héritage multiple). Mais il existe une solution. En analysant le code et en calculant tous les cas possible on peut quand même créer une table. D'ou un héritage multiple au même cout à l'execution que le simple.

Je rappelle qu'il est impossible du supprimer tout le temps la table. En effet l'héritage bien utilisé remplace des if dans le code. Dans ce cas il n'y a pas de surcout a utiliser le polymorphisme cela correspond juste au if qui a été supprimé.

J'espere avoir pas dit de connerie

Ben pour le moment c'est encore une version beta et c'est une version légerement modifé des unités qui est utilisé (XTA). Il y a eu un patch de proposé pour utiliser OTA (Original TA). Il n'y a que 4 cartes dans le jeux mais il y a eu 2 ou 3 carte proposée sur www.tauniverse.com qui reprenne des classique de ta (le format des cartes est legerement différent a cause du passage a la full3D). L'interface laisse une impression de bidouille.

MAIS c'est jouable et toutes les bases du jeu sont la et fonctionnelles ! De plus le but affiché est bien de retrouver le gameplay de ta et de supporter par la suite des mods extérieurs.

Pour ce qui est de la gaming zone de microsoft, ta spring ne fonctionne pas dessus et en bonus ils ont rajouté un petit logiciel pour chatter et lancer des parties ta spring. Bon il est programmé en C# (si je ne m'abuse) mais il suffirait d'en refaire un autre compatible pour lancer des parties sur n'importe quelle plateforme. On pourrait ainsi récuperer les joueurs perdus dans la zone de microsoft.

Pour ce qui est des probleme de copyright ils délivrent effectivement des donnés appartenant a ataris mais c'est le même problème que pour beaucoup de clone (celui de warcraft2, des lucas art, de duke nukem 3D) et a ma connaissance il y a uniquement eu des probléme avec blizard pour freecraft

Oui j'ai lu ses messages sur le forum de ta spring, j'ignorait qu'il avait un blog. Mais bon il doit se sentir un peu seul pour le moment bien que les développeurs de ta spring ne sont pas opposé a son projet (mais ils veulent quand même se consacrer a une seul architecture pour le moment - ce qui est tres sage d'ailleur). Et comme il le dit dans son blog ca a vraiment été réalisé avec des outils windows et on commence a parler de C# pour des logiciels annexes ...

Justement dans la meme soiré sur arte on apprenait que la cia n'avait à peut près que des conneries à son actif alors moi j'appellerai ça de la clairevoyance.

La lfjr c'était sur Kali, c'était un shareware pas trop cher. Kali servait surtout à rajouter le reseau IPX pour pouvoir jouer entre autre à War2 (BattleNet n'existait pas encore).

Perso j'ai surtout utilisé kali comme chat pour démarrer les partie de Total Annihilation. Comme TA utilisait DirectPlay on utilisaient directement les adresse IP. Pis après on c'est surtout servis d'ICQ.

>A propos de langage: le français tu en pense quoi? :)

Pas mal mais je prefere le lojban voir l'esperanto à la limite ;)

Bheua c'est simple oui mais chez moi en tout cas c'est pas impressionnant. D'ailleur ton prog est en train de tourner en fond pendant que je tape le message ... ;) cf le top : top - 01:00:14 up 2:46, 3 users, load average: 791.15, 273.00, 101.65 Tasks: 1039 total, 1007 running, 32 sleeping, 0 stopped, 0 zombie Cpu(s): 14.1% user, 85.9% system, 0.0% nice, 0.0% idle Mem: 126436k total, 124184k used, 2252k free, 3980k buffers Swap: 626492k total, 3844k used, 622648k free, 47348k cached PID USER PR NI VIRT RES SHR S %CPU %MEM TIME+ Command 4698 outs 16 0 1564 1564 1344 R 3.5 1.2 0:02.86 top 3635 root 15 0 94112 11m 2452 S 1.0 9.2 0:14.66 X 4700 outs 17 0 228 228 216 R 1.0 0.2 0:00.14 bloque 4702 outs 17 0 228 228 216 R 1.0 0.2 0:00.14 bloque 4703 outs 17 0 228 228 216 R 1.0 0.2 0:00.14 bloque [...] Je suis sur gentoo avec le noyau fournis par defaut et je n'ai fais aucune modif. Ca doit etre pasque ils onts patché le noyau.

>Ah la génétique, elle peut tout modifier, et même ..., ah bon, améliorer ?

Bha pour que les tomates retrouvent leur gout c'est plus simple que ça.
En fait comme les tomates sont cultivés hors-sol dans une serre avec une grosse dose d'engrais elles poussent très vite. Et a cause de ça elles n'ont pas le temps de créer les aromes normalement présents : comme il l'a dit c'est juste une boule pleine de flotte.

Tout ca a cause du systeme économique qui pousse les prix vers le bas.

De plus comme aucun insecte ou escargot n'arrive à en bouffer un petit bout elle n'ont pas de blessures et donc pas de déformations dans leur forme.

The ring ! :)

>qui n'est pas encore intégré dans la distribution standard

Et qui risque de ne jamais l'être à cause de la double license de mozilla et de l'utilisation de la bibliothèque libart qui elle est GPL. Je me demande pourquoi ils ne fonts pas un plug-in ca serais plus simple.

En plus le moteur de peut pas encore afficher les dégradés !!!

Ce qui serai cool c'est de prendre le moteur de sodipodi et d'en faire un plug-in ;)

Et puis il faut aussi compter avec la culture particulière des jeux video : celle ci est fortement ancré dans le propriétaire. Le plus le plus important dans le dévoloppement d'un produit libre c'est la création d'une communauté autour du logiciel. Et justement la création d'un jeu video est plus un processus à sens unique : il s'agit d'un équipe qui crée *son* jeu et qui ensuite le distribue aux joueurs sans que ceux ci ne veulent forcement chercher a y contribuer
Un peu comme on regarde un tableau ou un film : on regarde la vision/création de quelqu'un sur un thème donné.
Il existent des contres exemples comme les mod pour les FPS (comme counter strike et d'innombrable autres) mais c'est a chaque fois un produit qui est crée a partir d'un base déja faite.
Il n'existe aucun gros jeu open-source. Je pense comme toi que le développement en bazar est néamoins possible mais il faut bien se rendre compte que le jeu video n'est pas un terreau fertile pour.

C'est vrai mais son point de vue est différent, si l'émulation est un solution temporaire, dans ce cas elle est justifiée mais l'activité commercial de WineX rentre clairement en concurence avec le développement et le portage de jeu en natif (il y a des exemple concret dans l'interiew comme Wizardry8 et Kohan).

En plus pour faire tourner les jeux récents wine ne suffit il faut WineX qui est un logiciel propriétaire dont les auteurs se foutent pas mal du libre (ils onts récupéré les sources de wine pour leur compte et depuis wine est passé d'une licence type BSD a une licence GPL).

Et puis moi j'ai choisis les logiciels libres parceque ce sont les meilleurs ! Je ne veux pas d'un solution batarde, ce que je veux c'est les meilleurs jeux sous linux *et* en natif !! Et c'est ce que Simms fait et pas WineX

Je trouve aussi que Michael Simms a une bonne vision des choses, je trouve, en rejetant l'émulation. C'est utile pour jouer a des trucs dont la matériel à disparu, mais pour un jeu windows d'un point vue strictement informatique c'est vraiment rajouter une couche logiciel superflue : vive l'usine a gaz.

Et un plus il a bon gout car il a dis que Total Annihilation et Battlezone sont sur sa liste personnelle :)))

Vous parlez tous (presque) de "double license", à mon avis c'est incorect : un logiciel ne peut avoir qu'un seule license ! Surtout si, comme c'est le cas ici, elles sont contradictoires.
Il vaudrait mieux parler de deux versions différentes de "Multi Network Firewall", l'une libre l'autre propriétaire. Ce n'est pas juste un chipotage de vocabulaire cela signifie réellement qu'il y a une barrière entre les deux.
Contrairement a ce que j'ai pus lire au dessus si quelqu'un contribue à la version GPL Mandrake ne peut pas inclure la modifiation sauf si il recode complétement le patch par l'un de leur employé ou si il demande l'autorisation à l'auteur du patch (personnelement c'est une chose que je ferai uniquement contre rémunération).
Donc si MNF intéresse la communauté nous allons bientôt voir apparaitre une version libre différente de celle developpé par Mandrake.
Pour moi cela constitue bien un cadeau de Mandrake pour les logiciels libre puisque rien ne les aurait empeché de ne faire que la version propriétaire. Voir par exemple ce que fait Suse.

Personnelement la seul chose qui me dérange c'est que je ne pense pas qu'il est du ressort d'un éditeur de distribution linux du faire du propriétaire. Mais si l'on regarde Mandrake comme une sociétée de service proposant une nouveau produit basé sur un OS libre à destination des entreprises comme cela est présenté dans leur communiqué de presse (http://www.mandrakesoft.com/company/press/pr?n=/pr/products/2403(...)) cela me semble tout a fait a propos.

Rapelons que mandrake ne vis pas d'amour et d'eau fraiche et qu'ils n'onts toujours pas un exercice fiscal positif (http://www.mandrakesoft.com/company/investors/newsletter/sn021206(...)) c'est tout le mal que je leur souhaite.

A+

Cool on vas pouvoir tester ca pour le concour de la new juste en dessous ! :)

Ben presque si tu a le driver pour ta carte ethernet dans le noyau du média de boot et que ton FAI utilise DHCP ca fonctionne tout seul. Faut juste mettre les bonnes source apt (http).

Sinon le plus simple est sans doute de télécharger le premier cd de debian et d'installer la connexion apres le premier boot.

>http://www.google.fr/search?as_q=site%3Aopensou(...)

Google a recherché site:opensource.org GNU sur le Web.
2 résultats, sur un total d'environ 103

non 103 fois le mot GNU

>suite a lecture du comparatif, j'ai voulu apprendre Ocaml
>Mais j'ai fait un rejet d'Ocaml: je n'ai vraiment pas l'esprit fonctionnel.

Le rejet au début c'est normal la facon de penser est tellement diférente ...

Mais si tu t'accroche un petit peut tu verra que les outils que te proposent les languages fonctionnels sont *tres* puissant.
Quelques petits exemples :

- L'inférence des types : on ne définis jamais le type des variables (pas de définition et pas de typage de fonction non plus).
Le type est déterminé par le compilateur (on dit inféré) grace aux opérations qui sont effectué dessus.
Par exemple si on fais a+b le compilateur sait que a et b sont des integer car l'opérateur + ne s'applique qu'a eux.
Alors évidement c'est tres différent du C (la language de base pour bcp d'entre nous) mais imaginez comme c'est cool de ne pas avoir à déclarer des milliard de trucs ni a utiliser des caractères comme en perl (style $variable ou @bidule) (j'espere que je dis pas de connerire pasque ca fais des annés que j'ai pas touché au perl)

-La pleine fonctionnalitée : les fonctions sont des variables (presque) comme les autres. Grace à ça on peut définir des itérateur (des for améliorés) sur toutes les structures de donnés. Exemple : vous prenez l'itérateur do_list qui applique une fonction a tout les objet d'un liste, et vous pouvez faire :
do_list (printf "%s") ma_liste;;
et ca imprime toute la liste

Alors évidement le revers de la médaille c'est que les compilos de ce genre sont généralement assez lents. A mon avis ceux qui l'ont programmé doivent être très fiers de leurs optimisations. C'est vraiment un tour de force de faire tourner ca plus vite que du C++.

Et l'auteur du comparatif dis justement que la vitesse d'éxecution n'est pas tout : le temps de développement peut être aussi déterminant, et justement grace a la puissance d'Ocaml on peut avoir le beurre et l'argent du beurre =)

Et puis programmer en fonctionnel même juste pour essayer je trouve que ça ouvre l'esprit a d'autre méthode et d'autre facon de résoudre les problemes.

REHM Joris

Pour ceux que ca intéresse : caml.inria.fr (en plus c'est francais)