jeudi 24 juillet

Accueil :: Dépêches :: Archives :: Proposer une dépêche :: Journaux :: Forums :: Entretiens :: Suivi :: RDF

Derniers journaux de Montaigne :

[10/10@15:31] Le serveur de LinuxFr devrait être remplacé
[04/10@10:41] Création du projet "OQLToLang"
[02/10@21:36] Language naturel 2 python
[28/06@15:47] Les processeurs multicoeurs et l'avenir du développement
[07/06@11:25] Un OS réécrit son code à la volée
[30/05@16:02] L'expressivité des langages
[14/05@13:48] Ministère du civisme
[03/05@09:36] Où partir ?
[17/04@19:39] [HS]Un livre censuré fait le bilan de l'action de Nicolas Sarkozy
[17/04@16:21] A mort les boucles
[02/04@08:35] Le projet Isaac cherche un thésard (bourse de thèse)
[09/02@15:56] La FSF serait sur le point d'interdire à Novell de distribuer Linux
[17/10@12:35] [annonce]Formalisation grammaticale d'un pidgin
[13/09@08:12] La tribu
[17/08@12:03] Considération
[21/07@10:09] Le discours occidental vire t-il à la rhétorique ?
[11/05@21:28] Décidément "il" est partout...
[09/05@21:30] La PS3 en Novembre
[07/04@14:28] Choisir un environnement de dev pour y écrire un plugin
[12/03@21:26] Comment virer quelqu'un quand on veut.

Journal : Des langages de haut niveau

Posté par Ontologia (page perso, ) le 02 janvier 2008

Les langages de programmation actuellement utilisés par l'ensemble des développeurs, malgré l'amélioration des paradigmes et autres sucre syntaxiques , restent basés sur un certain nombres de primitives très restreint : Affectation d'une valeur en mémoire, calcul arithmétique sur celle-ci, branchement conditionnel.
Muni de ces axiomes, le code exécuté, même dans des langages fonctionnels, objet et autres, travaille sur les données qu'il possède à l'instant T, manipulant des contenus d'adresses mémoire : il s'agit d'une sémantique opérationnelle.

Les projets informatique grossissent, le nombre de bug et de coût de maintien avec, et c'est guère l'amélioration de sucre syntaxique ou paradigmatique des langages utilisés dans l'industrie, qui permettra de tenir la barre le plus longtemps possible.

Il y a deux ans, votre serviteur avait traduit les interview de Jarold Lanier et Victoria Livschitz , tous deux (à l'époque) chercheurs dans les laboratoires de SUN, critiquant le manque de sémantique des langages.
Jarold Lanier, en particulier, relevait judicieusement que les langages que l'on connait, ne sont que la virtualisation des câbles connectant les blocs logiques d'ordinateur primitifs comme l'ENIAC. Celui-ci préconisait une approche plus basé sur la reconnaissance de forme.

Victoria Livschitz répond à son collègue en déclarant que c'est le manque d'intuivité de la sémantique des langages de programmation modernes qui implique la difficulté de maîtrise des gros projets informatique.
Elle cite aussi l'impossibilité pour une brique logiciel de s'adapter à un nouvel environnement, et partant, de la difficulté de créer des architectures pérennes.
Le problème réside donc dans la sémantique des langages, et moins dans les méthodes de génie logiciel qui sont elles très étudiées.
Il n'y a qu'à voir tout l'engouement des journalistes et architectes pour les technologies SOA ( Source Wikipedia : Service_Oriented_Architecture) et autres méta-trucs.
Le talon d'achille de cette approche est que l'on retombe toujours sur du code classique : ce ne sont que des générateurs de code qu'il faut ensuite faire vivre, maintenir... quand le code généré a la qualité d'être lisible, voire non bogué..

Après quelques réflexions, principalement réalisées dans le cadre du projet Isaac, dont le langage offre des possibilités inédites et réjouissantes, j'en suis venu à vous proposer quelques mécanismes, issu de mon expérience personnelles et surtout professionnelle.
Je me contente de proposer quelques primitives de plus, principalement pensé pour des langages objets, mais probablement adaptable pour d'autres langages. Je ne suis pas à l'abri d'avoir réinventé la poudre, conçue ici et là. Certains mécanismes ne sont que la généralisation de concepts vu ailleurs.
Les utilisateurs de langage orientés aspect reconnaitront peut être des choses faisable avec cette approche, mais un des principes majeur de cette réflexion est d'essayer de rendre la programmation plus intuitive. Cela implique souvent des choix qui peuvent paraitre arbitraire : utiliser une syntaxe de type SQL dans un langage objet est sémantiquement équivalent à d'autres syntaxes plus adapté à la logique objet, mais surement moins intuitives, le SQL se rapprochant du langage naturel.
Il faut donc bien avoir à l'esprit que concevoir des briques pour langages de plus haut niveau est autant de l'informatique théorique que de la psychologie humaine : il faut rapprocher la sémantique d'un langage de l'imagination humaine et de sa psychologie.

Je précise un vocabulaire lisaacien que j'utiliserai dans le texte qui suit :
- Un objet ne doit pas être vu comme un objet d'un langage à classe. Il est cloné et non instancié, il peut changer dynamiquement de parents à l'exécution
- Un slot, est un élément d'un objet. C'est soit une donnée, soit une méthode. En Lisaac, une donnée peut devenir du code, et vice-versa.
- Un block est une fonction, ou peut être encore vu comme une liste d'instructions à évaluation retardée. Un block peut prendre plusieurs valeurs en argument et renvoyer plusieurs autres valeurs. Un bloc s'exécute lorsqu'on appel le message value. Bien évidemment, un block peut être promené un peu partout et exécuté comme on veut. Il peut aussi être transformé en donné (du type de données qu'il est censé renvoyer).
- la syntaxe - unevariable : TYPE := valeur_d_init [ code;]; représente une définition de la variable de unevariable de type TYPE, qui a l'initialisation vaudra valeur_d_init, et dont on définira un contrat, dont le code est contenu entre les crochet.
Ce code sera exécuté à chaque accès (en lecture ou écriture) sur la variable. C'est une sorte de primitive de type aspect. Nous pensons rajouter une primitive dans le compilateur permettant de n'exécuter du code que lorsque l'on écrit ou lit la variable, ce qui permettra d'éviter des traitement inutile. Pour plus d'information, se référer au manuel d'utilisateur de Lisaac

Commençons par le premier que j'ai pompé chez TrollTech. Vous avez sûrement deviné : le système de Slots/Signaux

Ce concept consiste à permettre à des élément d'interface graphique d'être connecté à la méthode d'un objet quelconque, afin de lui envoyer un message lorsqu'un évènement quelconque relatif audit élément survient.
L'intérêt est qu'on a pas à se trimbaler des références d'objet dans les diverses parties du code. On défini une connexion à l'initialisation, et il suffit ensuite d'écrire le code associé.
Ce modèle pose quelques problèmes dans une logique d'objet à classe, mais beaucoup moins dans une logique d'objet à prototype : en effet, un prototype n'est pas une définition formelle d'un objet qui deviendra vivant à l'instanciation, il est d'ors et déjà vivant dès que le programme début son exécution. Il n'y a donc pas de problème, à définir une connexion entre deux objets qui ne s'échangeront jamais leur référence.
Bien utilisé, cela permet une séparation propre du code selon un pattern MVC, en permettant en plus de threader tous les traitements.

Lisaac étant un langage permettant de rendre et prendre en argument des n-uplet typés, on pourrait imaginer des connecter des slot typés.
Par exemple, si l'on connecte un champ éditable d'interface utilisateur, et que l'on connecte l'évènement "modification du texte" à un slot, on pourra utiliser un signal qui renvoi la chaine du champ texte nouvellement modifié. Le slot connecté doit donc prendre une chaîne en argument.
C'est le compilateur qui fera la vérification de cohérence de type à la compilation.

evenement_changement_texte.connect block_a_executer;

Le mapping directionnel de données avec filtre

Très souvent dans les logiciels que j'ai eu à écrire, j'ai passé pas mal de temps à écrire de la glue entre éléments d'interfaces, voires objets, et organiser un système de rafraichissement, permettant de synchroniser deux couches d'objet, et autres variables. J'imagine que je suis loin d'être le seul...
Tous ces problèmes reviennent en réalité à définir une équation d'équivalence entre données.

Soit à poser axiomatiquement :
Donnée2 = fonction(Donnée1)

Ce mécanisme consiste donc à définir qu'un objet est toujours égal à un autre, via une relation fonctionnelle.
Cela implique, que toutes modifications de Donnée1 implique un traitement du type Donnée2 = fonction(Donnée1) mettant à jour le contenu de Donnée2, où qu'elle se trouve.

Cela peut être implémenté pratiquement grâce à des langages orientés aspect, comme AspectJ par exemple, où, en Lisaac, grâce à la possibilité de définir un contrat sur un slot, donc une variable.

liststr : LIST[STRING] := NULL [ Self := otherobject.unechaine.split ";"];
Ici, on défini que liststr est par définition otherobject.unechaine splité pour le ";". On est obligé (de par la syntaxe actuelle de Lisaac) de définir une valeur "de départ" pour ce slot.

Ce genre de détail à un intérêt majeur dans des interfaces de logiciel gestion, ou il suffira de définir des filtres entre les objets de la vue et du modèle, la vue se mettant à jour toute seule.

Une réflexivité sur les arbres

Lorsqu'on code, on travaille beaucoup sur les arbres, et force est de constater que c'est souvent galère.
Caml nous apporte deux outils fabuleux pour simplifier la difficulté : les types somme et le filtrage de type.

On peut définir un arbre très simplement :

type arbre = Feuille of string | Noeud of arbre;

Un filtrage de type nous aide ensuite à trier

let rec affichearbre = function
Feuille(s) -> print s
|
Noeud (n)-> affichearbre n;;

L'ajout de cette primitive éprouvée dans pas mal de langage aiderait souvent. On pourrait ensuite greffer d'autres mécanismes, existantes dans des logiciels comme CodeWorker.

La gestion du temps

En sémantique opérationnelle, le code exécuté à un instant T travail sur l'état de la mémoire à ce même instant T. Ceci implique que l'on doit en permanence mettre de côté des données, gérer des dépendances diverses et variées afin de simuler une possibilité qui nous semble naturelle pour l'esprit humain : recueillir des informations à partir des évènement de la vie passé, dont on se souvient

Un langage de très haut niveau possède une sémantique permettant de gérer la dimension supplémentaire qu'est le temps. On devrait pouvoir demander au programme de nous donner des informations calculée précédemment, mais sans nécessiter de les mettre de côté.
Prenons un exemple : on doit réaliser un traitement sur des milliers de fichiers XML (une petite manipulation de l'arbre). Ce traitement a la particularité de nécessiter deux passes, car le deuxième traitement, nécessite que le premier soit terminé sur tous les fichiers.
En effet, le document global est éclaté en milliers de fichiers qui s'appellent les uns les autres, on cherche à poser des liens hypertextes dans cette documentation à partir des données contenus dans les documents, puis à vérifier que ces liens sont bijectifs (un lien doit toujours renvoyer vers un document qui permet de revenir au document précédent).
On utilise un objet que l'on va créer pour chaque fichier et que le GC détruira pour nous.
Dans la sémantique du langage, on devrait pouvoir exprimer qu'une information donnée se trouve parmi tous les objets exécutés à tel endroit du code.

Lorsqu'un block de code contenant une boucle a exécuté un traitement sur tous les fichiers, on devrait pouvoir interroger ce block de code sur les liens qui ont été posés.

Pour illustrer certains autres mécanismes, je propose de jouer avec du pseudo-code autour de l'écriture de certaines partie d'un petit jeu de sous-marin : BlueWar est un vieux jeu des années 80 qui consistait à manoeuvrer un sous-marin pour descendre tous les bateaux ennemis qui trainait dans les parages. Ce jeu est sorti sur Amiga, Thomson TO8/TO9, et surement d'autres plateforme !
On disposait de plusieurs vues comme l'écran de commande, avec périscope, carburant disponible, lance torpille ou l'indispensable carte dynamique sur laquelle on voyait se déplacer tous les bateaux.
Vous pourrez avoir une idée de ce qu'était la première version de ce jeu sur Thomson TO8, en regardant quelques screenshot : http://www.logicielsmoto.com/viewsoftware.php?softid=57

Selon un modèle Vue-Agents, ce logiciel comporte

Une vue périscopique avec
- Profondeur
- Charge des batteries, niveau de réservoir
- niveau d'oxygène
- 2 indicateurs de torpille
- Direction
- Voyant avarie

Une vue radar

Une carte marine dynamique

On défini le terrain de jeu :

Agents/sma.li (le sytème multi agent dans son ensemble)



 - mysubmarine : SELFSUBMARINE;

 - vaisseau_ami : LIST[VAISSEAUAMI];

 - vaisseauennemi : LIST[VAISSEAUENNEMI];

Puis le sous-marin que l'on va commander :

Agents/selfsubmarine.li :



Section Private



- time : TIME;

- profondeur : INTEGER := 0;

- charge_batterie : INTEGER;

- niveau_reservoir : INTEGER := 0 [Self := Self.modulo 300];

- moteur_electrique : BOOLEAN;

- vect_direction : VECT2D [(Self.module_zero > 1).if { warning "Attention, le module du vecteur direction n'est pas à 1 !\n"};];

- torpille_prete_à_lancer1, torpille_prete_à_lancer2,avarie : BOOLEAN;

- niveau_oxygene := 0 [Self := Self.modulo 100];

- vitesse : INTEGER;

- position : VECT2D [TIME.each_second {Self := Self+vitesse*vect_direction};]; // On colle une équation liant position, vitesse et direction

- pression_trop_importante : BOOLEAN := FALSE;

- periscope : BOOLEAN; // périscope utilisable en surface;

Equation d'Etat

Il arrive très souvent que l'on ait besoin de programmer une machine à état plus ou moins complexe. Ce qui est particulièrement pénible en procédurale, l'est beaucoup moins avec un langage objet. Mais cet exercice reste encore souvent fastidieux. On aimerait pouvoir définir un ensemble d'équations d'état, qui, du moment qu'elle sont cohérentes entre elle (et c'est là qu'on déplacera la difficulté), permet de définir un agent animé et autonome.

J'utilise mon exemple de jeu BlueWar, pour décrire, par l'exemple, ce que pourrai être une définition d'état.
La syntaxe, inspirée du langage Lisaac est totalement fictive et n'est même pas une proposition, prière de ne donc pas la commenter.

On définit une section dans le code où l'on va "poser" les "équations"

Section State

La section State ne définie pas des fonctions destinées à être appelées, mais des fonctions d'état fonctionnant à la manière d'un flip-flop : une fois enclenchée un état A, seul l'enclenchement d'un autre état B, avec une équation spécifiant que l'enclenchement B annule l'état de A, arrête cet état A.

Un état n'est donc pas un morceau de code exécuté à un instant T, mais la manière d'être de l'objet/agent, durable.
Je vois donc deux type de code définissable dans un agent :
- Soit l'exécution d'une équation d'état
- Soit l'exécution d'un block selon une équation de temps (que ce soit une fois par seconde ou plus souvent/irrégulièrement). Ce block sera donc réexécuté selon l'équation temporelle. Elle définira l'animation de l'agent.

On a les propriétés suivante pour un état
- Un état est paralellisable
- Un état est démarrable ou stopable arbitrairement.
- Un état est démarrable ou stopable par une équation d'état.

On définie ici une équation entre 3 états :

- gestionprofondeur : STATE_EQUATION := plonger ^ remonter ^ maintenirprofondeur;
On a ici défini que le sous-marin soit remonte à la surface, plonge, ou se maintient à la même profondeur (ou exclusif).



- init <- // appelé à la création

(



	 	TIME.each_minute { 

			  moteur_electrique.if {

				   charge_batterie := charge_batterie - 2;

				   } else { // La combustion consomme de l'oxygène

					   niveau_oxygene := niveau_oxygene - 2;

					   niveau_oxygene := niveau_reservoir - 2;

				   };

	};



);

Définition des 3 états :



- plonge <-

(

	TIME.each_second { profondeur := profondeur - 5;};



 {profondeur > 300) => {pression_trop_importante := TRUE; plonge.off;}; // le sous-marin implose à cause de la trop grande pression

	

);

- remonte <-
(
// Code a exécuter à intervals réguliers
TIME.each_second { profondeur := profondeur + 5} until {profondeur := 0};

// Equation d'état
(profondeur = 0) => {
maintient_profondeur.on; // on démarre l'état "maintient_profondeur"
remonte.off; // on stop l'état "remonte"
};
);

La logique d'une définition d'état n'étant pas la même, il faut bien voir qu'on a ici deux définition parallèle, et non successives : toutes les secondes la profondeur du sous-marin va diminuer et l'équation sera régulièrement testé.
L'idéal serait que le compilateur réécrive le code de sorte que l'équation d'état soit exécuté à la suite du block {profondeur := 0}, car cela évite des tests régulier.



- maintien_profondeur <-

(

	// A la surface on recharge les réserves en oxygène.

	(profondeur = 0).if {

		 niveau_oxygene := 100;

		 périscope := TRUE;

	};

);

On revient à du code plus classique où l'on définie les slots d'un objet :



Section Public



- set_direction nb : INTEGER <- // converti orientation horloge -> vecteur 2D

(

	 vect_direction.x := (nb*pi/6).cos; 

	 vect_direction.y := (nb*pi/6).sin;

);



- lance_une_torpille <-

(

 // ...

);

On défini 3 objets, sans leur code :

Agents/vaisseau.li

Agents/vaisseauEnnemi.li hérite de vaisseau

Agents/VaisseauAmi.li hérite de vaisseau

Le radar

View/Radar.li

On définie ici un mapping de données directionnelles, avec filtre :



radar : LIST[VECT2D] [select position from sma.vaisseau_ennemi, sma.vaisseau_ami where (position.module sma.mysubmarine) < 100;];

On notera qu'on a ici utilisé une requête OQL afin sélectionner les vaisseaux se trouvant dans un disque de 100 de rayon autour de mysubmarine

View/Carte.li



- points_vaisseaux : LIST[VECT2D] [Self := select position from sma.vaisseau_ennemi, sma.vaisseau_ami;];

L'ensemble des primitives que je propose ici sont assez difficile à exécuter pour un interpréteur et encore plus à compiler, en particulier pour les sémantiques de gestion d'état et d'interrogation de données sur traitement effectués dans le passé.
Cela nécessite une nouvelle race de compilateur doté d'une intelligence artificielle, capable de détecter pas mal d'incohérence dans le code et ainsi de prévenir des code qui s'emballent, boucles, et autres comportement ingérable.
Cela nécessitera aussi d'autres méta-machins, pardon méthode de modélisation et gestion de projets informatique.

L'avenir nous dira si tout cela est possible.

> Lire le journal (91 commentaires, moyenne: 1,6).

Cette discussion est archivée, il n'est plus possible de laisser des commentaires.

Note : les commentaires appartiennent à ceux qui les ont postés. Nous n'en sommes pas responsables.

Plusieurs problèmes avec tes primitves

Posté par Jerome Herman () le 03/01/2008 à 05:08. (lien). Évalué à 2.

Le problème principal qu'il y a à interfacer un cerveau humain avec un ordinateur est que l'ordinateur est une machine à calculer alors que le cerveau est une machine à reconnaitre (tellement puissante qu'elle peut même par le jeu de description reconnaitre des choses qu'elle n'a jamais rencontré auparavant). Au jour d'aujourd'hui toute la puissance de la machine réside dans sa bétise intégrale : elle n'interprète absolument pas ce qu'on lui donne et fait ce qu'on a demandé même si c'est idiot. C'est surpuissant car 1°) celà garanti un fonctionnement cohérent 2°) celà permet au programmeur (la plupart du temps équipé d'une machine à reconnaitre) de comprendre ce qui se passe exactement en morcelant le déroulement pour trouver les erreurs.

Les gros inconvennients de tes paradigmes est qu'ils imposent une interpretation non triviale de l'intention du programmeur. Aujourd'hui c'est techniquement infaisable et pour le futur je ne suis pas sur que celà soit souhaitable. Il est extrèmement délicat de méler affectation, variables et contrats pour plusieurs raisons.
La première est que l'ordre d'évaluation change tout, par exemple si je commence par valider mes contrats, puis que j'affecte mes états, puis que j'évalue mes variables rien ne me dit qu'à la fin de l'évaluation des variables mes contrats sont encore valide... De plus si j'évalue mes variables puis que je valide mes contrats rien ne me dit non plus qu'une des validation n'a pas modifié une variable qui invalide un contrat précédamment validé etc. Pour finir variable -> etat -> contrat n'a pas forcément le même résultat que contrat -> etat -> variable.
La seconde est que lorsque les variables, contrat et etats s'inter-affectent il est horriblement complexe (en fait impossible si le langage est Turing complet) de valider qu'il n'y a pas de référence circulaire ou de deadlock
Par exemple : [(soleil = visible), (pluie=non), (température > 20°c)] -> {il fait beau} -> {il fait jour et chaud} -> [(soleil = visible), (pluie=non), (température > 20°c)]
Il est nécessaire qu'une personne décide si le contrat affecte l'état, ou si c'est l'état qui valide le contrat ou encore si ce sont les variables qui valide le contrat qui à son tour affecte l'état. La machine ne peut pas prendre cette décision.
Or là on touche le problème de fond, le troisième problème, demandez à un être humain si c'est parcequ'un nombre est négatif qu'on met un signe moins devant ou si c'est parcequ'il y a un signe moins devant qu'on le considère comme négatif et il risque un peu de faire la tête. En fait l'interpretation est décidée en fonction de l'ordre dans lequel arrive les données. -4 est recconu comme valeur négative de quatre et valeur négative de quatre est transcrite comme -4. Pour recalquer ce comportement à un système informatique il faut éclater la notion de variable en trois notions :
- l'unité
- la donnée
- la valeur.
L'unité pourrait être vue comme un méta-ensemble de types, c'est ce qui fixe le cadre de ce dont on est en train de parler. Un bonne exemple d'unité serait "vitesse du sous-marin A exprimée en km/h et évaluée à l'instant t=T+2min et 30 seconde de jeu"
La donnée est le contenu de l'unité, c'est à dire soit une information arbitraire saisie ou décidée à l'initialisation, soit le résultat d'une suite de calcul ou d'évènement sur cette donnée.
La valeur est la justification de la donnée en d'autre terme ce qui permet de faire la différence entre un -4 que l'on interprère en nombre quatre en négatif et un nombre quatre en négatif que l'on note -4. bref tout ce qui permet de décider mathématiquement de quoi la valeur est une conséquence et quelles seront ses causes et donc ultimement de décider de l'ordre d'évaluation juste.

Bon il est 5h du mat, je suis pas sur d'avoir résussi à être clair...

--
Kha
root est un privilège, pas un droit !

[^]Re: Plusieurs problèmes avec tes primitves

Posté par Nicolas Boulay () le 03/01/2008 à 10:19. (lien). Évalué à 2.
"Bon il est 5h du mat, je suis pas sur d'avoir résussi à être clair..."

Je confirme. J'ai décroché après l'unité. Si l'unité serait les km/h, je n voix pas ce qu'est la donné ou la valeur. Qui est le "5" de "5 km/h" et dans ce cas que représente l'autre concept ?
- [^]Re: Plusieurs problèmes avec tes primitves
  
  Posté par Jerome Herman () le 03/01/2008 à 13:44. (lien). Évalué à 2.
  Je confirme. J'ai décroché après l'unité. Si l'unité serait les km/h, je n voix pas ce qu'est la donné ou la valeur. Qui est le "5" de "5 km/h" et dans ce cas que représente l'autre concept ?
  
  L'unité c'est la déclaration exaustive de ce à quoi se rattache notre variable. Dans le cas d'une vitesse par exemple ca ne serait pas simplement "km/h" mais "km/h rattaché à tel objet calculé à tel moment".
  La donnée c'est le 5 dans ton exemple. C'est la partie la plus facile du trio.
  La valeur c'est le contexte. Comment a-t-on trouvé la donnée ? A-t-on fait appel à une méthode de type object.getproperty, est-ce une valeur de référence utilisé en comparaison dans un contrat, est-ce un calcul fait à partir d'éléments publics ou privés de l'objet etc. En fait la valeur contient toutes les informations dont le compilateur et/ou programme va avoir besoin pour déterminer dans quel ordre il doit lancer ses évaluations.
  
  Par exemple une voiture qui accèlère sur une autoroute. Dans cette voiture le conducteur controle régulièrement la vitesse pour être sur de ne pas dépasser la limitation, et si c'est le cas il ralenti jusqu'à ce que la vitesse redescende en dessous de la limitation.
  
  Intuitivement le problème est très simple à poser en terme de contrats/etats/variables :
  
  Contrat principal : respecter la limitation de vitesse
  - 1ere Condition de réalisation du contrat : la vitesse constatée par le conducteur est inférieure à la vitesse limite
  - 2eme condition de réalisation du contrat : le conducteur vérifie la vitesse fréquament.
  
  Etats
  - vitesse inférieure à la limite
  - vitesse supérieure à la limite
  
  Variables
  - limitation de vitesse
  - vitesse du véhicule
  
  Le problème est que ce qui est naturel pour l'humain ne l'est pas pour l'ordinateur. Posé comme celà l'ordinateur n'a aucune façon de savoir si c'est parceque la voiture change de vitesse qu'elle respecte la limitation ou si c'est parcequ'elle respecte la limitation qu'elle change la vitesse. L'ordinateur étant idiot on peut supposer qu'il va évaluer le problème à l'envers et tendre vers l'état stable :
  Contrat respecté => vitesse inférieure à la limite => accélération et ne plus en bouger.
  Si un évènement entrainne un changement de vitesse limite (le conducteur sort de l'autoroute par exemple) l'ordinateur qui voit une variable changer arbitrairement va alors la rechanger arbitrairement ou changer arbitrairement l'autre de façon à garder la première condition valide. Du point de vue de la logique mathématique le problème est parfaitement résolu, par contre le programmeur risque de faire un peu la gueule en voyant le comportement de son programme.
  
  C'est là que la dichotomie valeur/donnée permet de résoudre le problème.
  On cherche à comparer deux unités qui sont
  "suite de chiffre inscrit sur un panneau concernant le tronçon de route sur lequel roule l'utilisateur" et "vitesse de la voiture telle que constaté par le conducteur quand il regarde à l'instant t"
  Les valeurs de ces deux unités sont
  "donnée aribitraire fixé par la direction départementale" et "résultat du calcul fonction de la donnée au temps t-1 et de l'accélération du véhicule "
  Les données sont (par exemple) 70 et 85
  Avec une sémantique adéquate on peut alors faire comprendre au système que la seule action possible sur la vitesse est un changement de l'acceleration du véhicule. De fait l'ordre de résolution est
  Etat impacte variable entrainne contrat.
  
  13h40 en espérant avoir été plus clair.
  
  --
  Kha
  root est un privilège, pas un droit !

[^]Re: Plusieurs problèmes avec tes primitves

Posté par Ontologia (page perso, ) le 12/01/2008 à 17:49. (lien). Évalué à 2.
Tu met le doigt sur un problème que je n'avais pas vu, tout à la définition de mon sous-marin muni de sa cohérence intrinsèque. Je suis heureux de ta réponse, car c'est un peu ce que j'esperais en le publiant ici :-)
En fait, tu relèves que mon modèle ne permet pas de définir un code déterministe.

Pourquoi cette erreur ?
- Parce que je mélange une sémantique axiomatique et une sémantique opérationnelle
- Parce que je n'ai pas vu que si j'utilisais certes mes contrats sur variable pour définir des compréhensions d'ensemble, je n'ai pas vu que sémantiquement on peut tout faire, et surtout n'importe quoi.

Donc que faire ?

J'en ai discuté avec Benoit (Sonntag, l'auteur de Lisaac), qui m'a conseiller de regarder la [[Méthode_B]].
J'en suis donc venu à étudier les possibilités de la méthode B évènementielle qui "colle" à peu près ce que je veux faire.

Mise à part que la syntaxe est absolument immonde (on ferait mieux de lui substituer une syntaxe du type OCL), le B évènementiel permet de définir des variables, définir leur ensemble d'appartenance et l'ensemble des états de l'automate. Le compilateur B permet de vérifier de la cohérence logique du modèle pour ensuite générer le code correspondant.

Le problème est qu'il est impossible de mélanger les deux sémantique, à moins qu'on ai la certitude qu'il n'y ait pas d'interférence entre elles (un cas valide pourrait être le fait que le passage à un état implique un appel d'une fonction graphique, qui ne renvoi rien et ne modifie pas l'état interne de l'automate).

Pour ceux, que ça intéresse, un cours assez clair ici : http://www.lri.fr/~paulin/B/poly002.html

Une perspective envisageable serait d'adapter les primitives de B évènementiel, avec éventuellement quelques sucres syntaxiques pour modéliser les états d'agent comme je les ai introduit ici.

En tout cas, encore merci, et je vais réfléchir à tout cela :-)

Les trous de lIsaac

Posté par gloups () le 03/01/2008 à 09:09. (lien). Évalué à 1.

Curieux de tous les langages qui augmentent le degré d'abstraction, qui facilitent la relecture et qui limitent le nombre d'erreurs de manière auto, j'ai décidé de jeter un petit coup d'oeil à Lisaac. Visiblement destiné à de l'embarqué, on est très loin de ce que propose un ruby pour de la gestion, il possède nombre de qualité qui réduit fortement le coût de codage par rapport à du C. Il intégre la notion d'agent, cela me parait efffectivement une bonne piste pour cette cible.

Etant néophyte sur ce lisaac, je me suis limité à parcourir les doc et faire quelques tests typiques. Voici mes premières remarques sur les limite du pouvoir d'expression de lisaac actuellement :

- Pas d'élément de rupture de séquences (type return, exit ,...). S'il est facile de substituer ces éléments par des tests, il n'en est pas de même pour la lecture. Cela me parait un manque, il serait souhaitable que le compilo prenne en charge cette transformation.

- Je n'ai pas vu de notion d'exception (pas à la java, mais plutot à la ADA) ce qui permettrait de remonter correctement les erreurs provenant des couches basses sans ajouter une nuée de tests partout. J'en profite pour dire que gestion d'exception ne doit pas être simplement une gestion d'erreur comme cela a été implementé dans de nombreux langages. La programmation par exception releve plus du concept évènementiel et entrerait totalament dans la philosophie de lissaac de ce point de vue.
La gestion d'exception permettrait également de mieux traiter les retours d'erreurs. Un exemple, une fonction C embeddée dans le core provoque une erreur, j'obtiens actuellement un magnifique "core dump" lisaac pas très corporate ;-); Une exception me permettrait de trapper l'erreur et de prendre la décision adéquat. C'est une chose indispensable si le logiciel doit s'auto-géré.
Une dernière remarque sur l'intégration d'exception aux langages, le traitement d'exception doit faire partie intégrante de la structure de bloc du langage pour être lisible (les try catch et autres syntaxes de ce genre sont à prohiber..., l'approche ADA est certainement la meilleure sur ce point)

- Dans la même veine, les pre et post conditions peuvent être une réponse élégante aux conditions "exceptionnelles" (à rapprocher de la gestion d'exception). Dans ce contexte, elle ne doivent pas seulement être cantonnée au debug. Je verrais bien des pre/pro conditions + et - liée au débug ou toujours activée qui déclancherait des exceptions trappable.
Ainsi, si j'ai la fonction log avec comme pré-condition x > 0, Je ne doit pas avoir à faire de tests pour une valeur saisie < 0, une exception doit pouvoir être générée et trappé au moins pour relancer le processus.

Ces quelques manques liés à la jeunesse du langage devrait permettre faire augmenter le niveau d'abstraction de lisaac.

Sinon Bravo, c'est un bon début et la gestion des agents me semble une piste prometteuse.

[^]Re: Les trous de lIsaac

Posté par Nicolas Boulay () le 03/01/2008 à 10:24. (lien). Évalué à 3.
Pour le 1er point, je crois qu'il y a une bonne raison que j'ai oublié :)

pour le 2), cela revient à la gestion signal/slot plus généraliste non ? Concernant le fait de rattraper les erreurs d'une fonction C embarqué, tu en demandes beaucoup. Je ne suis pas sur qu'un setjump/longjump avec récupération des signaux soit suffisant pour rattraper du C compilé.

Je crois que le 3 est faisable à travers des contacts, non ?
- [^]Re: Les trous de lIsaac
  
  Posté par Ontologia (page perso, ) le 03/01/2008 à 18:15. (lien). Évalué à 2.
  Pour le premier point, c'est tout simplement parce que le concepteur de Lisaac, considère que les mots clés du type break, etc... permettent à de très mauvaises habitudes de se développer.
  
  Le return car cela permet de faire quitter la fonction en plein de milieu de celle-ci, ce qui est très mauvais. Le break, car tu sort d'une boucle n'importe comment.
  
  J'évite d'utiliser ce genre d'ecueuil dans mon code, au début ça a été dur, mais au final, ça me simplifie la vie au debugging (moins de surprise).
  - [^]Re: Les trous de lIsaac
    
    Posté par TImaniac (page perso, ) le 03/01/2008 à 18:39. (lien). Évalué à 1.
    "Le return car cela permet de faire quitter la fonction en plein de milieu de celle-ci, ce qui est très mauvais."
    Pourquoi ?
    "Le break, car tu sort d'une boucle n'importe comment."
    Cad ?
    
    --
    MonoFrance
    - [^]Re: Les trous de lIsaac
      
      Posté par gloups () le 03/01/2008 à 22:48. (lien). Évalué à 0.
      Effectivement, il est toujours possible de coder sans rupture de sequence, toutefois cela est souvent au détriment de la clarté de l'algorithme.
      Un deuxieme argument souvent présenté est la difficulté de prouver le code contenant des ruptures... Il s'agit d'un probleme d'analyse de code donc hors de notre contexte...
      
      Sachant qu'un code est ecrit une fois et re-lu N-fois durant la vie du programme en maintenance, je privilégie la facilité de relecture.
      Une succession de tests complexes est plus lisible avec des break qu'avec une succession de clause else qui perdent leur sens au bout de 3 ou 4 conditions...
      
      Un langage se voulant de haut niveau comme Lisaac me semble devoir faciliter la vie du codeur pour exprimer le plus simplement possible l'algorithme; le reste de la tuyauterie doit être le domaine de l'optimisation et du controle du compilo.
      Pour qu'un langage soit attractif face aux langages installés, il est nécessaire qu'il puisse offrir les mêmes facilités, un pouvoir d'expression plus important (le minimum de mots nécessaires pour décrire un concept) et être lisible (un algo doit pouvoir s'écrire le plus naturellement possible).
      Il me parait curieux, d'apporter des contextes très avancés comme ceux présentés dans cet article en laissant à coté des lourdeurs syntaxiques qui rebuteront nombre de programmeurs.

[^]Re: Les trous de lIsaac

Posté par kaouete (page perso, ) le 03/01/2008 à 10:56. (lien). Évalué à 2.
J'y connais pas grand chose : En quoi les exceptions de ADA diffèrent de celles du c# ou du java ?

J'ai lu hier cet article très intéressant [1] qui démonte les exceptions de ces deux derniers langages, est-ce que c'est le même problème avec ADA ?

[1] http://blogs.msdn.com/oldnewthing/archive/2005/01/14/352949.(...) sur lequel je suis tombé en lisant ce très intéressant (bis :) article mais un peu long [2]
[2] http://www.joelonsoftware.com/articles/Wrong.html
- [^]Re: Les trous de lIsaac
  
  Posté par Pierre Tramonson () le 03/01/2008 à 13:33. (lien). Évalué à 2.
  Je ne vois pas en quoi cet article démonte les exceptions C# et Java, ni en quoi il démonte le besoin d'exceptions tout court.
  
  Gérer des exceptions n'empêche absolument pas de gérer des erreurs ou des débranchements possibles à coup de if.
  En particulier son It's really hard to write good exception-based code since you have to check every single line of code (indeed, every sub-expression) and think about what exceptions it might raise and how your code will react to it., je ne vois pas en quoi c'est spécifique aux exceptions.
  Et au passage, Java force à catcher les exceptions qui sont susceptibles d'être levées (et signale qui à quelle ligne peut en provoquer une), donc le think about en est grandement facilité.
  - [^]Re: Les trous de lIsaac
    
    Posté par kaouete (page perso, ) le 03/01/2008 à 14:54. (lien). Évalué à 1.
    Pour répondre à ta première phrase, de mon point de vue, l'article montre qu'il est plus difficile de faire un bon code avec exception qu'un bon code avec une gestion des erreurs à la main (maintenant je dis pas que l'un est mieux que l'autre, mais que les exceptions c'est galère :)
    
    Maintenant, pour avoir coder en java en essayant d'exploiter les exceptions à fond, c'est vrai que ça devient *très* rapidement un truc ultra lourd avec des millions de try/catch de throw, et qu'il est toujours complexe de tout bien prendre en compte. Dès qu'on appelle une fonction il faut pas simplement catcher les exceptions (ce que Java t'oblige à faire de toute façon) mais aussi *réfléchir* à comment les gérer, et pire, comment *bien* les gérer.
    
    Pour moi tout ça montre que les exceptions, c'est pas la panacée pour gérer les erreurs, et donc je me demandais comment était utilisée les exceptions dans ADA :)
- [^]Re: Les trous de lIsaac
  
  Posté par gloups () le 03/01/2008 à 23:17. (lien). Évalué à 2.
  Il s'agit encore d'un problème de lisibilité et non de défense d'ADA.
  En ADA chaque bloc possède implicitement un section exception qui fait partie de la structure syntaxique. Il est donc aisé de mettre en oeuvre une exception; la programmation par exception est alors réalisable pour exprimer clairement un algorithme et ses conditions d'arrêts qui peuvent être analysés à differents niveaux y compris au niveau le plus haut pour re-initialisé un système par exemple.
  
  Begin
  ...
  Exception:
  excep1 => traitement1()
  End
  
  Les langages plus récents ont cantonnés les exceptions à de la gestion d'erreurs tout en voulant adjoindre une mécanique de remontée d'informations. Ceci est louable mais alourdi considérablement la syntaxe au point de ne pouvoir l'utiliser pour autre chose de la gestion d'erreurs. Il suffit d'imbriquer 2 ou 3 blocs d'exception en Java pour se rendre compte du probleme.
  
  Dans un système temps réel, les conditions d'arrêt sont multiples et souvent provenant de cause hors logiciel, il est plus simple de lâcher une exception et de la trapper au niveau adéquat pour reprendre le traitement sans devoir gérer la pile d'erreurs en cascade en retour de chaque fonction.

[^]Re: Les trous de lIsaac

Posté par GTof (Jabber id, ) le 03/01/2008 à 11:36. (lien). Évalué à 2.
Une manière élégante et très puissante de gérer les execptions est d'utiliser des monades. Le concept brièvement c'est :

Une fontion f d'un type A dans un type B qui peut générer une exception de type C peut être vu comme une fonction sans exception du type A dans le type "une valeur B ou une exception C". Mettons qu'on ai deux fonctions comme ca: f et g que l'on veut composer ou executer séquentiellement, l'idée c'est d'avoir un opérateur (disons >>= ) pour lier les deux (f >>= g) de telle sorte que si f renvoie une valeur B on passe a g et si elle renvoie l'exception, on n'execute pas g et on renvoie directement C.

Est ce que les block de Lisaac peuent être vu comme des fonctions anonymes ? Si oui Lisaac devrait le supporter et donc avoir des exceptions. Je suis tombé sur un article intéressant décrivant des monades pour Ruby [1], comme quoi les monades sa sert partout.

[1] http://moonbase.rydia.net/mental/writings/programming/monads(...)

[^]Re: Les trous de lIsaac

Posté par sonntag () le 04/01/2008 à 03:45. (lien). Évalué à 2.
Tout d'abord merci d'avoir regardé de près le Lisaac.

L'absence de Break ou de Return ou d'exception ont été un choix délicat :
1) Ce sont des ruptures de contexte, donc des "goto" cachés. La garantie de linéarité
du code est quelque chose d'important au niveau génie logiciel.
(Il aide aussi à l'analyse de flot et la recherche de preuve sur le code)
2) Lorsque nous avons un langage ayant la programmation par contrat, cette linéarité
est aussi importante : nous garantissons l'exécution des pré, du code, puis des posts
sans se poser de question d'interruption. Il s'est avéré qu'il était bien agréable de ne pas
avoir besoin d'analyser tout le code d'un fonction pour ajouter une action à la fin de
celle-ci.
C'est le choix de Bertrand Meyer, multe fois argumenté dans son livre et directement mise en oeuvre dans son langage Eiffel.
3) la sortie par break ou par return dans une imbrication importante de code est un signe
d'un code mal fragmenté (découpage insuffisant en fonctions). Cette absence incite le
programmeur à fragmenter plus son code pour le rendre plus lisible.
J'ai comme vous beaucoup programmé avec la possibilité de return ou de break,
mais après une période de sevrage (En Eiffel, puis en Lisaac), j'apprécie cette absence...
4) Le choix d'un langage minimaliste : ce qui n'est pas indispensable n'est pas ajouté.
C'est un choix de goût, ou plutôt de philosophie. Le Lisaac a une grammaire plus petite
que SmallTalk et n'a rien à voir avec celle de Java ou C#...
Nous ajoutons que si cela est indispensable ! Plus le langage est petit et uniforme dans sa
façon de penser, moins il est difficile à comprendre ou à apprendre...
Evidemment, pour être d'accord avec cela, il ne faut pas avoir la philosophie suivante :
"Un langage est facile a comprendre ou apprendre si il ressemble à ce que je connais !"
(Qui est la philosophie de Java ou C# avec leurs syntaxes proche du C.)
Ici, ma philosophie fonctionne mieux si on considère que la personne ne connais rien.
(c'est dans cette même idée que SmallTalk, avec Squeak, est considéré comme un langage destiné aux enfants)

Pour les exceptions, la programmation par contrat recouvre en partie, et de manière plus
élégante, l'utilisation des exceptions.
Mais, je te l'accord, ce n'est qu'en partie...
L'utilisation des Blocks à évaluation retardé ou "closure" (introduit en Lisp) recouvre encore une autre partie de l'utilisation des exceptions.
Il reste peut être encore des trous dans notre approche, qu'il va falloir analyser avec
beaucoup de précaution pour ne pas faire redondance et ne pas inclure une brique qui
va à l'encontre du génie logiciel.
L'approche des exceptions en Java n'est clairement pas la bonne, et nous avons l'air
d'être d'accord sur ce point, il faut donc y réfléchir... (pourquoi voir plutôt vers ADA)

Ce sont des débats assez délicats comme : "langage typé vs langage non typé" ou encore
le choix d'avoir une syntaxe drastique sur les majuscules et minuscules...
Cela reste des choses argumentables , mais c'est aussi des trous sans fin à discussions philosophique. Nous avons une philosophie bien précise autour du Lisaac, nous essayons
de nous en tenir pour réaliser un langage racé de qualité dans sa catégorie, et non un
langage four tout n'ayant plus d'âme. :-)
- [^]Gestion d'erreur lisaac
  
  Posté par gloups () le 04/01/2008 à 12:30. (lien). Évalué à 2.
  Je suis totalement en phase avec cette dernière approche, c'est une des raisons pour laquelle je m'interesse à lisaac.
  
  Pour les break/return ..., je ne suis pas certain que l'on puisse l'assimiler à un goto qui est explicitement une mauvaise pratique, je l'assimilerai plus à une simplification de conditionnelles imbriquées, pratique de mon point de vue saine, d'ailleurs die_with_code() existe et effectue cette action bien au delà du bloc puisqu'il s'agit de la sortie intégrale du programme.
  Mais il semble s'agir effectivement d'un choix conceptuel déjà tranché, aussi je ne reviendrais plus dessus.
  
  Je souhaiterai par contre revenir sur la gestion d'erreur de manière plus générale. Contexte dans lequel les exceptions fournissent une solution élégante à la problématique :
  1. La gestion d'erreur ne devrait pas être attaché uniquement à une phase debug, nombre de circonstances provoquent des erreurs, souvent lié au logiciel ou matériel sous-jacent, donc difficilement contrôlable et anticipable.
  Prenons l'exemple de lisaac qui s'appuie sur des lib C, en cas d'erreur de la lib, lisaac devrait fournir un mécanisme permettant de trapper l'erreur et prendre la décision adéquat. Quelques types par defaut existent généralement (erreur de contrainte, Div/0, systeme, ...) .
  Un de mes premiers tests lisaac a été l'utilisation de la ligne de commande, étonnant non ;-) ...; en itérant un cran trop loin (trop classique...), j'ai eu le droit à un magnifique core dump... . Je m'attendais plutot à erreur de contrainte ou erreur de Fctn sous-jacentes beaucoup plus explicite.
  
  2. Le traitement d'erreur n'est pas forcement réalisé au même niveau que la détection et de survenance de l'évènement.. Il est donc nécessaire de pouvoir remonté la pile des appels.
  Dans un système complexe, toutes les interactions ne sont pas forcement déterministe (en particulier quand on s'interface avec des éléments externes, il est alors pertinent d'avoir un mécanisme générique et simple d'emploi sans devoir spécifier à tous les étages les types d'erreurs attendus ... ;-)
  
  3. Afin d'être traiter convenablement, l'information de contexte d'erreur doit exister au moment du traitement.
  
  4. Une exception doit pouvoir remonter la pile d'exécution, jusqu'à son traitement éventuel.Si ce n'est le cas, le programme s'arrête avec sa pile d'exécution classique.
  
  Dans ce contexte, Lisaac possède quelques embryons intéressants :
  1. La programmation par contrat couvre effectivement bien la partie déclenchement d'exception à condition que l'on puisse ajouter un contrat sur affection de valeur et non uniquement en pre et post condition. Dans ce cas, de manière déclarative, il est possible d'exprimer une contrainte qui sera sujette à erreur et donc déclenchement d'exception.
  
  Un exemple classique simpliste, la lecture d'un capteur doit retourné une valeur entre 1 et 10, Lors de la lecture, une valeur de 0 ou 11 déclenche une exception qui interrompra les appels en cours, jusqu'au niveau du controleur du système qui trappera l'exception pour re-initialiser convenable le capteur.
  
  Dans ce cas, en pseudo algo, cela peut être ecrit :
  ... Valeur = lecture() si Valeur <1 ou Valeur > 10 alors raise Hors_limite; ...
  Je préfere nettement, la vision déclarative qui sépare nettement les cas d'erreurs ou exceptionnels de l'algo nominale sans pour autant terminer l'application.
  Header : Check Valeur < 1 ou Valeur > 10, sinon exception Hors_limite Code : ... Valeur = lecture() ...
  
  2. La propagation et la capture de l'exception reste à définir. Le contexte de remontée ne doit pas créer de nouveaux objets (difficile en cas de memoire pleine...) mais devrait plutot s'appuyer sur un contexte statique réservé à cet usage.
  
  3. Dans une vision volontairement unifiée, les exceptions pourraient apporter à lisaac :
  - un mécanisme générique de remontée d'erreur :
  - émis par les contrats, pouvant être utilisé en debug mais également en production.
  - émis volontairement par le programmeur
  - être le support générique de terminaison de bloc, méthode ou programme.
  
  Sur les exceptions ADA (dans le même esprit que cellede PL/1).
  La structure de l'exception ADA est a la fois :
  - intrégré dans la structure syntaxique (fait partie intégrante du bloc)
  - simple d'usage
  - Le contexte transmis est statique, une exception levée et trappée doit être traité avant q'une autre puisse être levée. ceci évite les tentation de traitement complexe dans l'exception.....
  pour aller plus loin dans ce sens, un commentaire sur le sujet :
  http://www.les-ziboux.rasama.org/faq-ada-presentation.html#e(...)
  - [^]Re: Gestion d'erreur lisaac
    
    Posté par Nicolas Boulay () le 04/01/2008 à 14:16. (lien). Évalué à 3.
    Franchement je préfaire largement la gestion signal/slot.
    
    Par contre, il faut faire attention aux contrats: ils sont censé être sans effet de bord !

Hein ?

Posté par alenvers () le 03/01/2008 à 11:08. (lien). Évalué à 2.

>Muni de ces axiomes, le code exécuté, même dans des langages
>fonctionnels, objet et autres, travaille sur les données qu'il possède à
>l'instant T, manipulant des contenus d'adresses mémoire : il s'agit
>d'une sémantique opérationnelle.

Tu mélanges le code produit et sémantique du langage lui-même.

Les processeurs actuels possèdent un jeu d'instruction impératif, appelé par ailleurs parfois opérations. C'est donc logique que le "code executé", comme tu dis le soit fait de façon opérationnelle puisque que le hardware sous-jacent ne sait rien faire d'autre.

Pour ce qui est des langages, les langages fonctionnels ne sont pas définis par une logique d'état mais par un notion de fonction ; c'est à dire, plus ou moins, par une correspondance entre les entrées et les sorties, peu importe la boite noire qui effectue cette transformation, l'important c'est la correspondance entrée-sortie (qui est déterministe).

On ne définit pas les langages fonctionnels en terme d'opération, d'étape mais en terme d'entrée et de sortie (un correspondance) ! Cela est du ressort, par exemple d'un sémantique dénotationnelle pas opérationnelle.

Le compilateur, d'un langage fonctionnel, quant à lui, effectue une correspondance entre le langage fonctionnel (à sem. dénotationnelle) et le langage machine (à sem. opérationnelle). Cette correspondance est, par ailleurs, une approximation (car pas de nombre infini, pas de précision infinie, ...).

[^]Re: Hein ?

Posté par Vivi (page perso, ) le 03/01/2008 à 14:00. (lien). Évalué à 1.
Cela est du ressort, par exemple d'un sémantique dénotationnelle pas opérationnelle.

pas forcèment, on peut avoir une sémantique opérationnelle pour un langage fonctionel aussi (cf. la sémantique opérationnelle du lambda calcul).
- [^]Re: Hein ?
  
  Posté par alenvers () le 03/01/2008 à 14:13. (lien). Évalué à 2.
  Evidement qu'il est possible d'avoir un sémantique opérationnelle (pour un langage fonctionnelle (sinon, il serait vraiment pas facile d'écrire un compilateur qui est censé produire du code qui est orienté opérationnel).
  
  Mais procéder de la sorte dénature la paradigme fonctionnel. Un peu comme écrire du OO/Fonctionnel/autres en C, c'est possible, mais c'est laid.

[^]Re: Hein ?

Posté par Axioplase Ashi (page perso, ) le 05/01/2008 à 23:40. (lien). Évalué à 1.
C'est tout à fait ce que je me disais. Il faisait (pas forcément volontairement, à chacun sa spécialité) l'omission des paradigmes fondamentaux de la prog fonctionnelle.
Le meilleur exemple étant sans doute quand il parle de ses "équations qui s'équilibrent". J'appelle ça littéralement un point fixe.

Il faut se dire quand même que si nombre de langages pèchent par absence de sémantique, on ne peut pas vraiment dire ça des langages fonctionnels (sauf de Caml, où la sémantique, c'est le code du compilo ^^).
C'est un bel exemple d'une branche de l'info où l'on passe plus de temps sans ordi qu'avec ordi, pour développer un concept, et il n'y a pas de place pour le debuggage à chaud (comptez-donc le temps écoulé pour l'aboutissement de Scheme R6RS)...

Bref, j'ai rien codé en Lissac encore, mais j'attendrai d'avoir un peu de formalisme derrière avant de m'y lancer (ne le prend pas mal, j'ai pas lu tes publis encore non plus)

--
J'aime la liberté.
J'aime BSD.

Heu...

Posté par Antoine () le 04/01/2008 à 00:11. (lien). Évalué à 1.

Jarold Lanier [...] préconisait une approche plus basé sur la reconnaissance de forme.

Victoria Livschitz [...] cite aussi l'impossibilité pour une brique logiciel de s'adapter à un nouvel environnement, et partant, de la difficulté de créer des architectures pérennes.

Eh bien, j'espère que tes amis ont une carte de fidélité au bistrot du coin.
Comme dit Gombrowicz : « plus c'est intelligent, plus c'est con ! ».

[un objet] peut changer dynamiquement de parents à l'exécution

En Python, tu peux changer la classe d'un objet en affectant simplement l'attribut __class__, mais c'est une pratique considérée comme fort crade.

il faut bien voir qu'on a ici deux définition parallèle, et non successives

Tu peux regarder comment fonctionne VHDL, qui a exactement cette sémantique.

C'est trop compliqué !

Posté par Philippe Fremy (page perso, ) le 04/01/2008 à 10:25. (lien). Évalué à 1.

Le problème de fond des langages de haut niveau est qu'ils sont difficiles à appréhender par le commun des mortels. Aussi bien soient-ils, ils demandent de penser différemment. Au final, un langage impératif est quelque chose de vraiment facile à assimiler. Donc bien que ce soit une source d'erreurs, comme c'est _vraiment_ facile à comprendre, c'est ce que les gens apprennent.

Les gens qui se posent un peu la questions d'approches différentes de la programmation, notamment avec des langages utilisant des concepts différents sont en général ceux qui déjà dans leur pratique de la programmation sont très rigoureux.

Quand on propose à un étudiant qui vient de faire trois années pour apprendre péniblement le java de faire du lisp, ça lui sort par les yeux.

Pour reprendre ton exemple du sous-marin, tu peux dire que le sous-marin a trois états et que décider de plonger, c'est faire un changement d'état global qui entraine des mises à jour automatiques en cascade, pour le commun des mortels, c'est plus simple de dire qu'on donne l'ordre au sous-marin de plonger et qu'il faut faire des trucs pour ça. La description impérative est tout simplement beaucoup plus simple à appréhender, même si elle est beaucoup plus sujette à une erreur lors de la mise en oeuvre.

--
phil.freehackers.org

[^]Re: C'est trop compliqué !

Posté par Ontologia (page perso, ) le 04/01/2008 à 16:55. (lien). Évalué à 2.
Oui, je suis d'accord.

D'aileurs, on aurait jamais du inventer la locomotive à vapeur, parce qu'une carriole tirée par des chevaux, c'est beaucoup plus simple.
C'est vrai ! C'est compliqué une locomotive à vapeur ! Tout ce jeu complexe de température, de pression, d'étanchéïté...

Les inventeurs de cette machine auraient du arrêter tout de suite !

Tiens mais pourquoi ont-ils continués ?
- [^]Re: C'est trop compliqué !
  
  Posté par TImaniac (page perso, ) le 04/01/2008 à 17:23. (lien). Évalué à 1.
  Parcqu'au final c'est pas plus compliqué de conduire une locomotive que de s'occuper de chevaux ? Que le gain de confort/vitesse/sécurité est indéniable et conséquent ? Parcqu'il permet de transporter bien plus de personnes et de marchandises ?
  Lissac n'apportera jamais un facteur 10x en vitesse par rapport au langage C, il n'apportera pas la sécurité qu'apporte un programme écrit en B ou même en Java, il ne permettra pas d'écrire des programmes plus complexes que dans un autre langage (la limite étant surtout liée aux compétences humaines et non techniques), etc.
  
  --
  MonoFrance
  - [^]Re: C'est trop compliqué !
    
    Posté par Nicolas Boulay () le 04/01/2008 à 17:47. (lien). Évalué à 2.
    "il n'apportera pas la sécurité qu'apporte un programme écrit en B ou même en Java,"
    
    Il faudra argumenter un peu plus tout de même...
    
    Ou alors, c'est juste une tentative de troll de plus ?
    
    il ne permettra pas d'écrire des programmes plus complexes que dans un autre langage (la limite étant surtout liée aux compétences humaines et non techniques),
    
    C'est sûr qu'il n'y a aucune différence de productivité entre l'assembleur et le C, le C et Java, Java et Perl.
    
    Petit trolleur !
    - [^]Re: C'est trop compliqué !
      
      Posté par TImaniac (page perso, ) le 04/01/2008 à 18:23. (lien). Évalué à 1.
      Il faudra argumenter un peu plus tout de même...
      Bah un programme écrit en B peut être prouvé, donc même s'il génère du code "natif", il est vérifiable "à priori" (évidemment les spec du programment restent écrites par un humain...). C'est plus une sécurité vis-à-vis d'un plantage "non prévu".
      Pour Java, il y a une couche d'abstraction entre le code généré et le code réellement exécuté, autorisant un certain nombre de vérifications supplémentaire par rapport à un programme natif compilé à partir d'un langage autorisant à peu prêt tout et n'importe quoi comme accès bas niveau. C'est une sécurité (toute relative) vis-à-vis de certains types d'erreur de programmation mais aussi une sécurité vis-à-vis de code malveillants.
      
      C'est sûr qu'il n'y a aucune différence de productivité entre l'assembleur et le C, le C et Java, Java et Perl.
      J'ai pas parlé de productivité mais de complexité. Globalement il est tout à fait possible de faire des grosses applications en C/C++ ou en Java comme il est sans doute possible de le faire en Lissac, mais ce dernier ne va pas apporter grand chose comme a pu apporter la locomotive par rapport à la charette.
      
      --
      MonoFrance
      - [^]Re: C'est trop compliqué !
        
        Posté par Jerome Herman () le 05/01/2008 à 01:25. (lien). Évalué à 1.
        Bah un programme écrit en B peut être prouvé.
        Il va fallor donner des exemples de langages de programmation turing complet ET non prouvable. Le B possède des outils et uen sémantique qui facilitent la preuve mathématique, mais à partir du moment ou on a un code turing complet et un compilateur/interpreteur déterministe on peut prouver un code. Le contraire serait inquiétant.
        
        C'est plus une sécurité vis-à-vis d'un plantage "non prévu".
        La preuve permet de certifier un comportement, mais ne met pas à l'abri des plantages loin de là. Elle garantie juste que si il n'y a pas d'éléments extérieurs au programme qui viennent le perturber le programme finira et donnera un résultat cohérent (celui ci pouvant bien sur être une remontée d'exception). Or des éléments perturbateur il y en a un paquet : problèmes de droits, réponse incohérente d'un composant (typiquement lors de transactions réseau ou IPC), changement de contexte suite à une interruption dans une opération non atomique, dead-lock sur des ressources extérieures au programme et j'en passe. Quand il s'agit de prouver un système (ie le programme, les programmes qui tournent à coté, l'os sous jacent et le matériel) c'est une autre paire de manche... Et là le B n'aide pas particulièrement.
        
        Pour Java, il y a une couche d'abstraction entre le code généré et le code réellement exécuté, autorisant un certain nombre de vérifications supplémentaire par rapport à un programme natif compilé à partir d'un langage autorisant à peu prêt tout et n'importe quoi comme accès bas niveau
        De deux choses l'une, soit tu devellopes pour windows Me/98/95 soit je suis au regret de t'apprendre qu'un programme écrit en Java a exactement les mêmes droits qu'un programme écrit en C. Le langage Java n'apporte rien au niveau limitation d'accès bas niveau par rapport au langage C. On peut par exemple aller écrire (essayer en tout cas) dans un ségement de mémoire qui ne nous appartient pas. Si l'OS est bien foutu il sortira le fusil à pompe et on aura un mort sur la consicence. Le framework java permet de limiter la casse sur les plus grosses erreurs, mais il existe aussi d'excellents frameworks en C avec garbage collector et controle des I/O qui font un super boulot quand il s'agit de hurler à la compilation plutôt qu'à l'execution.
        
        mais ce dernier ne va pas apporter grand chose comme a pu apporter la locomotive par rapport à la charette.
        Pour bien comprendre ce qu'apporte un langage comme Lissac par rapport à un langage comme C il faut penser aux non programmeurs. Pour être honnête je en connais pas Lissac, mais l'avantage majeur des langages de haut niveau est de permettre à des non initiés de modifier facilement une partie du programme suivant leur besoin. De même qu'un cube de données bien que plus lourd qu'une base est plus facile à manipuler, il m'a été donné uen fois dans ma vie de coder un logiciel en prog dont les prédicats étaient librement accessibles aux utilisateurs qui disposaient également d'un shell réduit pour appeler les fonctions quia vaient étés codées. Moyennant une formation légère d'une semaine, les utilisateurs pouvaient aussi bien évaluer les faits réels que lancer des simulations en pagaille. La même chose en C ou en Java aurait nécessité le dévellopement complet d'une interface doublée d'un parseur interpreteur ou l'action systématique d'un developpeur à chaque fois qu'un utilisateur aurait voulu changer une règle de calcul ou une relation entre objets.
        
        --
        Kha
        root est un privilège, pas un droit !
        
        [^]Re: C'est trop compliqué !
        
        Posté par Yusei (page perso, ) le 05/01/2008 à 10:13. (lien). Évalué à 2.
        
        à partir du moment ou on a un code turing complet et un compilateur/interpreteur déterministe on peut prouver un code. Le contraire serait inquiétant.
        
        Peut-être faudrait-il préciser ce qu'on entend par "prouver", parce que pour moi, même prouver qu'un programme s'arrête, c'est balaise... alors prouver qu'il fait bien ce que l'on veut...
        
        Peut-être parlais-tu de prouver que le code produit est bien "identique" au code source ?
        
        [^]Re: C'est trop compliqué !
        
        Posté par Jerome Herman () le 05/01/2008 à 11:35. (lien). Évalué à 1.
        Peut-être faudrait-il préciser ce qu'on entend par "prouver", parce que pour moi, même prouver qu'un programme s'arrête, c'est balaise
        
        C'est faire un algorithme capable de vérifier si un programme s'arrête ou non qui est balèze. Prouver qu'un programme s'arrête peut être très simple.
        Par exemple le programme composé de la seule instruction exit(0); s'arrête de façon triviale. Pour les programmes plus complexes ca se résoud à coup de théorie des graphs, de validations algorithmiques et/ou de calculabilité.
        
        Certaines méthodes sont plus faciles à prouver que d'autre. L'approche récursive par exemple est très facile à prouver. Prouver un programme revient à regarder l'ensemble des états qu'il peut traverser (éventuellement l'ensemble des états que chacune de ses fonctions peut traverser) et à vérifier pour chaque état ou pour chaque ensemble d'état que l'état suivant est bien valide.
        
        --
        Kha
        root est un privilège, pas un droit !
        
        [^]Re: C'est trop compliqué !
        
        Posté par Yusei (page perso, ) le 05/01/2008 à 12:03. (lien). Évalué à 2.
        Il y a une différence entre dire "peut être simple à faire" et "est faisable". Ce n'est pas parce que quelque chose est simple dans certains cas que c'est toujours faisable.
        
        Quand tu dis qu'à partir du moment où on a un langage Turing complet, on peut prouver le code, je ne comprends pas "dans certains cas, c'est facile".
        
        Si tu confirmes que dans ce que tu appelles "prouver le code", on peut inclure "prouver que le programme se termine", alors ton hypothèse "on peut prouver n'importe quel programme d'une machine de Turing" repose sur le fait que le cerveau humain est plus puissant qu'une machine de Turing.
        
        [^]Re: C'est trop compliqué !
        
        Posté par Jerome Herman () le 05/01/2008 à 12:29. (lien). Évalué à 1.
        Si tu confirmes que dans ce que tu appelles "prouver le code", on peut inclure "prouver que le programme se termine",
        
        La preuve n'est pas forcément vraie. Prouver qu'un programme se termine ne veut pas dire démontrer qu'un programme se termine. Quand on prouve un code on peut prouver qu'il est vrai OU qu'il est faux...
        Quand on prouve un programme on cherche à savoir si oui ou non il fait ce qui est marqué sur la fiche de specs. C'est cette information supplémentaire qui permet de faire la preuve.
        
        On ne peut pas écrire un programme qui valide la terminaison ou non de tous les autres programmes car il est impossible de spécifier à priori l'ensemble de toutes les specs de tous les programmes. Par contre sur un programme donné, dont on connait par avance les specs et les états souhaitables il est possible (même programmatiquement) de voir
        a) Si on ne rencontre effectivement que des états souhaitables
        b) Si on termine le programme.
        
        Avant d'arriver au b) il faut d'abord valider le a) sinon on se retrouve avec un programme dont on ne connait pas les specs et de fait on est bien en peine de démontrer si il va boucler ou non vu que son comportement n'est plus formalisé. Par contre une fois que l'on a le a) et donc un nombre d'état possible limité, prouver le b) n'est qu'une question de temps.
        
        --
        Kha
        root est un privilège, pas un droit !
        
        [^]Re: C'est trop compliqué !
        
        Posté par Yusei (page perso, ) le 05/01/2008 à 12:54. (lien). Évalué à 2.
        
        La preuve n'est pas forcément vraie.
        
        Une preuve fausse n'a pas beaucoup d'intérêt.
        
        Prouver qu'un programme se termine ne veut pas dire démontrer qu'un programme se termine.
        
        Tu peux aussi démontrer qu'il ne se termine pas. Mais dans la plupart des cas, tu ne pourras démontrer ni l'un ni l'autre, et c'est tout le problème.
        
        Par contre sur un programme donné, dont on connait par avance les specs et les états souhaitables il est possible (même programmatiquement) de voir
        a) Si on ne rencontre effectivement que des états souhaitables
        b) Si on termine le programme.
        
        Par état souhaitable, tu veux dire état dont on sait qu'il mêne au bon résultat (et à une terminaison du programme) ? Si c'est le cas, alors la détermination des états souhaitables revient à prouver le programme, et est impossible dans le cas général par quelque chose de puissance équivalente à une machine de Turing (MT).
        
        prouver le b) n'est qu'une question de temps.
        
        Prouver qu'un programme termine (sur un jeu de données fixé) n'est qu'une question de temps: il suffit de l'exécuter. Prouver qu'un programme ne termine pas est une autre paire de manches.
        
        Je pense qu'il est temps de recentrer un peu le débat, car on s'éloigne un peu. Tu disais que du moment qu'on a un langage Turing complet, on peut prouver ses programmes. Or, tout langage Turing complet permet de produire des programmes dont on ne peut pas prouver la terminaison avec quelque chose de la même puissance qu'une MT.
        
        Je ne sais pas comment expliquer ça de manière plus claire. Tu as l'air de penser qu'à partir du moment où on choisit un programme en particulier, alors il devient prouvable. Ce n'est vrai que dans des cas particuliers. Il n'est pas possible d'écrire un programme validant la terminaison d'un autre programme quelconque. Tu peux penser qu'un humain peut le faire, mais ça suppose que la thèse de Church-Turing est fausse. En tout cas, une MT ne peut pas le faire, c'est un résultat mathématique bien établi.
        
        [^]Re: C'est trop compliqué !
        
        Posté par Jerome Herman () le 05/01/2008 à 15:03. (lien). Évalué à 1.
        Une preuve fausse n'a pas beaucoup d'intérêt.
        Si, on sait qu'on peut foutre le programme à la poubelle, ou au moins le corriger pour le rendre valide.
        
        Mais dans la plupart des cas, tu ne pourras démontrer ni l'un ni l'autre, et c'est tout le problème.
        Oui mais la réponse "on sait pas" => preuve fausse. Merci de revoir votre copie messieurs les programmeurs.
        
        Par état souhaitable, tu veux dire état dont on sait qu'il mêne au bon résultat (et à une terminaison du programme) ? Si c'est le cas, alors la détermination des états souhaitables revient à prouver le programme,
        
        Pas tout à fait, mais c'est vrai que c'est le plus gros du boulot.
        un état souhaitable est par exemple : variable d'entrée comprise entre 0 et 1, variable de sortie de type booléen contenant vrai ou faux. Après il faut encore démontrer que la variable de sortie est bien la bonne d'après les specs ie que le code de calcul est juste.
        
        et est impossible dans le cas général par quelque chose de puissance équivalente à une machine de Turing (MT).
        
        Dans le cas général oui.
        
        Prouver qu'un programme termine (sur un jeu de données fixé) n'est qu'une question de temps: il suffit de l'exécuter
        
        Euh non pas du tout. C'est pas parcequ'il s'execute une fois, qu'il le fera forcément la fois d'après même avec le même jeu de données. Tout un tas de question de concurrence et de priorité entrent en jeu. Sans même parler des problèmes liés au threads ou à l'OS sous jacent.
        
        Prouver qu'un programme ne termine pas est une autre paire de manches.
        
        Une fois de plus ca dépend du programme, il y a tout un tas de programmes qui ne terminent pas de façon tout à fait triviale (etats qui bouclent dans un graph par exemple)
        
        Tu as l'air de penser qu'à partir du moment où on choisit un programme en particulier, alors il devient prouvable
        
        A partir du moment ou on a des specs non infinies (ce qui est quand même le cas général) pour ce programme oui. Une fois de plus prouver un programme revient à répondre à deux questions :
        - le programme suit-il les specs (oui/non)
        - peut on assurer que le programme va se terminer (oui/non)
        
        La réponse à la seconde question peut parfaitement être non. Des programmes comme le jeu de la vie sont de bons exemples. Les specs sont parfaitement respectées, les états des différentes fonctions sont parfaitement connus par contre dans le cas général on ne peut pas savoir si le programme va s'arréter ou non avant d'avoir vu le jeu de données initial. Si on a des specs inifinies (la grille peut avoir n'importe quelle taille, les données initiales peuvent prendre n'importe quelle valeur) on est dans la merde. Par contre si on a une grille de taille limitée par exemple il suffit de rajouter la condition "arrêt si on revient sur un des états précédents" pour être sur que le programme s'arrêtera forcément.
        dans les faits il est souvent facile de rajouter des conditions jusqu'à avoir des specs finies vu que l'ordinateur sur lequel tourne le programme n'est pas inifini...
        
        Il n'est pas possible d'écrire un programme validant la terminaison d'un autre programme quelconque
        
        Je n'ai jamais dit celà, par contre il est possible d'écrire un programme validant la terminaison d'un autre programme spécifique dont l'ensemble des données (interne et externe) sont bornées en taille mémoire. En d'autres termes une machine de Turing qui n'a pas une bande infinie...
        
        Démonstration simple, une machine de Turing ne possédant que N états possibles. On détermine que l'etat 0 est arrêt. On a N² transition possible d'un état à un autre (un état pouvant éventuellement boucler sur lui même, amis aucun etat ne peut une fois amener à l'état X et la fois d'après amener à l'état Y). Il y a donc au maximum N état initiaux suivi de (N-1)xN² transition possibles soit N^4-N³ ensembles programmes+données tous parfaitement déterminés. Pour savoir si ils terminent ou non, il suffit de regarder ce quis era fait dans un temps fini (mais plutôt long quand même il faut bien l'admettre)
        
        --
        Kha
        root est un privilège, pas un droit !
        
        [^]Re: C'est trop compliqué !
        
        Posté par Yusei (page perso, ) le 05/01/2008 à 17:23. (lien). Évalué à 2.
        Bon, désolé, j'avais préparé quelque chose de mieux écrit, et suite à un clic mal placé, j'ai tout perdu. Pour résumer:
        
        il est possible d'écrire un programme validant la terminaison d'un autre programme spécifique dont l'ensemble des données (interne et externe) sont bornées en taille mémoire. En d'autres termes une machine de Turing qui n'a pas une bande infinie...
        
        C'est ce que je disais plus haut, et à quoi tu répondais "euh non, pas du tout": tu peux toujours exécuter le programme et voir ce que ça donne. Si tu bornes la taille mémoire utilisable, que tu stockes tous les états complets du programme et qu'à chaque étape tu vérifies que tu ne retombes pas dans un état déjà visité, alors en un temps irréaliste et avec une mémoire irréaliste, tu peux savoir si ton programme s'est terminé ou pas pour ces données là.
        
        C'est un résultat relativement inutile. J'ose espérer que quand on parle de "preuve de programme" on essaye d'avoir une certaine généralité. Ici, on devra réappliquer la même procédure pour chaque nouveau jeu de données, et cette procédure ne fait rien économiser par rapport à exécuter le programme sans rien prouver.
        
        Malheureusement les résultats un peu généraux sont algorithmiquement indécidables.
        
        Pour conclure de mon côté, je renverrais les lecteurs intéressés, s'il en reste, vers le théorème de Rice pour plus de détails:
        http://en.wikipedia.org/wiki/Rice's_theorem
        http://fr.wikipedia.org/wiki/Th%C3%A9or%C3%A8me_de_Rice
        
        La page française mentionne l'indécidabilité algorithmique du problème suivant, par exemple: « le programme calcule un résultat correct par rapport à la spécification ».
        
        (Ce qui, encore une fois, ne veut pas dire que l'on ne peut jamais rien prouver. En restreignant les problèmes considérés, on peut se ramener à des cas gérables.)
        
        [^]Re: C'est trop compliqué !
        
        Posté par Jerome Herman () le 06/01/2008 à 02:28. (lien). Évalué à 1.
        C'est ce que je disais plus haut, et à quoi tu répondais "euh non, pas du tout": tu peux toujours exécuter le programme et voir ce que ça donne
        
        Ce qui m'ennuie avec cette phrase et qu'elle induit violamment en erreur. Dénombrer exhaustivement puis évaluer tous les états d'un programme n'est pas du tout équivalent avec l'execution d'un programme sur l'ensemble des jeu de données possibles à raison d'un million d'execution par jeu. Dans le second cas rien n'indique que l'on a effectivement couvert tous les états possibles. Un état particulier peut très bien ne se produire que dans certaines conditions très précises.
        Par exemple si on cumule des arrondis au delà de la limite du CPU, on peut parfaitement avoir un programme qui calcule juste sur un ordinateur et faux sur celui d'à coté.
        
        De plus il n'est pas question d'executer ici le programme, mais de valider ses etat. Celà se fait le plus souvent de façon totalement extérieure au programme. Enfin il ne s'agit pas de valider le programme pour un seul et unique jeu de données, mais pour un ensemble de données toutes bornées.
        Avec la doc du CPU et du compilateur il est souvent à peine plus complexe de valider un état pour X appartenant l'ensemble des entiers 32 bits que pour X = 5
        
        C'est un résultat relativement inutile
        Si on ne pouvait prouver que sur un seul jeu de données oui, mais comme on peut prouver sur n'importe quel jeu de données borné à partir du moment ou les variables dans les états sont elles-mêmes bornées c'est très très pratique. Comme aucun ordinateur n'a de mémoire ou de registre infini on peut démontrer au cas par cas sur n'importe quel problème. Il arrive même (approche orthogonale aux types) que l'on prouve vrai un programme qui traduit un algorihtme d'un problème indécidable par ce que l'on sait que l'on va forcément se prendre un Out of Memory ou un NaN avant de rentrer dans les cas problématiques.
        Un bonne exemple de prblème indécidable qui n'empêche pas des programmes d'être prouvé est le calcul par éléments finis. Si l'utilisateur du programme sort des etats calculables, le programme lui envoie un joli message d'erreur l'invitant à revoir sa copie. Et on construit des avions parfaitement fiables avec ces trucs là...
        
        Pour conclure de mon côté, je renverrais les lecteurs intéressés, s'il en reste, vers le théorème de Rice pour plus de détails:
        
        Une fois de plus le Theorème de Rice démontre que l'on ne peut pas écrire un unique programme P tel que pour tout programme source SPx on puisse avoir P(SPx) -> le programe se termine ou non ET le programme est conforme aux specs. Il ne dit absolument pas que pour un programme quelconque spécifié il est impossible d'écrire un autre programme qui le valide ou l'invalide. Et vraiment j'insiste sur le fait que si le programme (a) tourne en environnement limité il existe au moins un programme (b) qui le valide ou l'invalide (même si pour celà le programme doit tourner dans un environnement exponentiellement plus vaste que celui du programme (a))
        
        --
        Kha
        root est un privilège, pas un droit !
        
        [^]Re: C'est trop compliqué !
        
        Posté par Yusei (page perso, ) le 06/01/2008 à 12:15. (lien). Évalué à 2.
        Tu mélanges allégrement cas spécifiques et cas généraux, et je n'arrive plus à être sûr de ce que tu veux dire. Tu as l'air de penser qu'en exhibant des contre-exemples de programmes pouvant être prouvés, tu démontres quelque chose. Depuis le début, je dis que je suis d'accord sur le fait que des cas restreints peuvent être prouvables. Le problème vient quand tu généralises à tous les programmes écrits dans un langage Turing complet.
        
        Nous avons aussi un problème de compréhension au sujet du formalisme utilisé pour la discution. Je parle de machines de Turing, et d'états de machines de Turing, et toi tu me parles d'erreurs d'arrondi et de CPU. Ce n'est pas du tout mon domaine, et j'ajouterais que ça ne m'intéresse pas trop puisque, si on a des problèmes de prouvabilité au niveau des machines de Turing "parfaites", ce n'est pas en ajoutant des possibilités d'erreur au niveau du codage des nombres, ou des problèmes de concurrence, qu'on rendra les choses plus facilement prouvables.
        
        Il ne dit absolument pas que pour un programme quelconque spécifié il est impossible d'écrire un autre programme qui le valide ou l'invalide.
        
        S'il est possible pour un programme quelconque fixé d'écrire mécaniquement un programme qui le valide ou l'invalide, alors il est possible d'écrire un programme qui valide ou invalide tous les programmes.
        
        S'il est possible pour un programme quelconque de trouver un programme qui le valide ou l'invalide, mais qu'on ne peut pas mécaniser ce processus, alors cela revient à dire que c'est algorithmiquement indécidable. C'est donc un objectif inaccessible si la thèse de Church-Turing est vraie, on y revient.
        
        Si on restreint le problème comme tu le fais aux programmes utilisant une mémoire finie, on sort de l'infaisable théorique pour arriver dans l'infaisable pratique, ce qui nous fait une belle jambe. Ca devient faisable théoriquement parce qu'on peut essayer tous les états possibles du programme, mais je serais curieux de voir une méthode générale plus efficace.
        
        il ne s'agit pas de valider le programme pour un seul et unique jeu de données, mais pour un ensemble de données toutes bornées.
        
        Eh bien, soit tu pars d'un jeu de données initial et tu énumères les états en vérifiant qu'on ne revient jamais dans un état déjà visité, soit tu énumères tous les états atteignables et tu vérifies qu'aucun d'eux n'est sur un cycle. Je ne suis pas sûr qu'énumérer les états atteignables soit faisable en général sans énumérer toutes les données initiales possibles, ce qui reviendrait à exécuter le programme pour chaque jeu de données possible.
        
        Formulé plus simplement, ce que je ne vois pas, c'est comment tu prouves qu'un état n'est pas sur un cycle sans partir d'un état initial, avancer jusqu'à cet état, et prouver qu'ensuite on ne revient pas à un état déjà visité. (Par état, je parle d'un état d'une machine de turing associé à ce qui est écrit sur le ruban.)
        
        Typiquement ton programme est un graphe où les noeuds sont des états et les arêtes des transitions. Tu peux faire mieux qu'énumérer tous les états (et donc toutes les données possibles) à condition de pouvoir compacter plusieurs noeuds en un seul, c'est à dire qu'au lieu d'avoir des états de type: (X, d) avec d un jeu de données, tu auras des états de type (X, D) avec D un ensemble de jeux de données.
        
        Ce qui m'intrigue, c'est comment on pourrait faire cette compaction dans le cas général. Je n'ai pas de preuve formelle que ce soit impossible de le faire de manière plus efficace qu'en énumérant tout, mais intuitivement ça me semble évident.
        
        [^]Re: C'est trop compliqué !
        
        Posté par Nicolas Boulay () le 05/01/2008 à 20:24. (lien). Évalué à 2.
        "Une preuve fausse n'a pas beaucoup d'intérêt."
        Si, on sait qu'on peut foutre le programme à la poubelle, ou au moins le corriger pour le rendre valide.
        
        Je dirais même plus, c'est le plus utile !
        
        Il est souvent beaucoup plus facile de trouver un contre exemple à un moteur de preuve que de d'assurer que l'ensemble des possibles est couvert.
        
        De plus, d'un point de vue psychologie d'un programmeur, on comprend mieux une erreur avec le contre exemple qui force la correction. Si le programme rend "prouvé", il y a beaucoup de monde qui n'y croira pas.
        
        Cela signifie qu'il vaut mieux chercher "large" que tenter de prouver complètement des bouts minuscules.
        
        Les 2 téchniques que je connais c'est la résolution d'équation logiques SAT et les BDD (parcoure de tous les états possible).
        
        C'est le moyen de faire une preuve "définitive" mais qui finit toujours par exploser en temps. Dans ce cas, des méthodes basé sur un montecarlo peut tout à fait fonctionner pour trouver un contre exemple.
        
        [^]Re: C'est trop compliqué !
        
        Posté par Thomas Douillard () le 07/01/2008 à 14:15. (lien). Évalué à 2.
        
        Par contre si on a une grille de taille limitée par exemple il suffit de rajouter la condition "arrêt si on revient sur un des états précédents" pour être sur que le programme s'arrêtera forcément.
        
        Ouais enfin pour le coup tu tombes un peu sur des problèmes de mémoire, genre t'es obligé de te souvenir de tous les états précédents ... et de temps de calcul (t'es obligé de comparer à chaque fois ton état courant avec tous les états précédents) et les états précédents rien qu'au jeu de la vie t'en a potentiellement 2^n, avec n le nombre de cellules.
        
        Donc en bourrin tu dois déja avoir une jolie complexité en temps et en mémoire.
        
        [^]Re: C'est trop compliqué !
        
        Posté par Ontologia (page perso, ) le 05/01/2008 à 18:08. (lien). Évalué à 2.
        Je pense qu'il est temps de recentrer un peu le débat, car on s'éloigne un peu. Tu disais que du moment qu'on a un langage Turing complet, on peut prouver ses programmes. Or, tout langage Turing complet permet de produire des programmes dont on ne peut pas prouver la terminaison avec quelque chose de la même puissance qu'une MT.
        
        C'est, il me semble, une application du théorème d'incomplétude de Godël.
        
        [^]Re: C'est trop compliqué !
        
        Posté par TImaniac (page perso, ) le 05/01/2008 à 10:30. (lien). Évalué à 1.
        . Le contraire serait inquiétant.
        Je ne prétend rien du tout, ni dans un sens ou dans l'autre. Je dis juste que la méthode B permet de prouver le programme écrit, l'environnement t'embêtant jusqu'à ce que t'es prouvé l'intégralité de ton code. En C t'as aucune contrainte à la compilation, et à l'exécution il n'y a que l'OS pour effectuer des contrôles de sécurité.
        
        La preuve permet de certifier un comportement, mais ne met pas à l'abri des plantages loin de là.
        Pas besoin d'étaler ta science, j'ai jamais dit le contraire. Je dis juste que ca offre une meilleure sécurité. Il est évident qu'on n'est pas à l'abris des comportements extérieurs au programme, à commencer par ceux du matos. J'ai également cité le problème des spécifications qui sont toujours rédigées par un humain.
        
        je suis au regret de t'apprendre qu'un programme écrit en Java a exactement les mêmes droits qu'un programme écrit en C.
        Je te mets au défi d'écrire un programme en Java pur (pas d'appel à du code natif hein) qui va taper n'importe où dans la mémoire ailleur que là où elle est autorisé par l'espace que lui a allouée la VM. Tu peux pas sortir des sentiers battus (sauf faille dans la VM bien entendu), et la première barrière n'est pas l'OS mais bien l'environnement contrôlé par la VM.
        Idem pour une application en ActionScript ou en C# par exemple. Le modèle de VM intermédiaire facilite grandement la vérification du code à exxécuter, et permet d'accorder plus ou moins de confiance et de droit à celui-ci. L'OS constitue une autre barrière qui vient éventuellement combler les lacunes du modèle et de l'implémentation de la VM, mais dans l'absolu ces langages offrent plus de sécurité qu'un programme écrit en C.
        
        Le framework java permet de limiter la casse sur les plus grosses erreurs
        Euh... t'appelle quoi le "framework" ? Si c'est juste l'ensemble des libs, je vois pas le rapport.
        
        Pour être honnête je en connais pas Lissac, mais l'avantage majeur des langages de haut niveau est de permettre à des non initiés de modifier facilement une partie du programme suivant leur besoin.
        Y'a des outils adaptés pour ca : moteurs de règles, moteurs de script avec langage métier dédié, etc. Lisaac se veut un langage généraliste (dans sa grammaire en tout cas), et ca c'est déjà imbittable pour la plupart des non développeurs.
        
        --
        MonoFrance
        
        [^]Re: C'est trop compliqué !
        
        Posté par Jerome Herman () le 05/01/2008 à 12:12. (lien). Évalué à 1.
        Pas besoin d'étaler ta science,
        Je n'étale pas ma science, mais d'un coté tu dis que les langages de haut niveau sont trop complexes et n'apportent rien et de l'autre tu donnes des exemples de langages de plus haut niveau que le C qui apportent des plus en terme de sécurité, de calreté de code ou de prouvabilité. Choisi ton camps camarade. Tout ce que je dis est que du point de vue de l'OS peut importe que ce soit un programme en C ou un programme tournant sur une JVM, les droits seront les mêmes, les erreurs potentielles aussi.
        
        Je te mets au défi d'écrire un programme en Java pur (pas d'appel à du code natif hein)
        Je prend ton "pas d'appel à du code natif" comme une interdiction d'utiliser des commandes extérieures à java. Cependant pour aller en dehors de la zone mémoire allouée, il va quand même falloir taper sur des appels systèmes à l'OS.
        
        La façon la plus simple de faire celà est d'aller modifier le bytecode d'une des classe de base. Ca se fait très bien avec javassist par exemple : http://www.csg.is.titech.ac.jp/~chiba/javassist/
        Cette bibliothèque java permet de changer à la volée les noms, les méthodes et dans une certaine mesure les types des classes chargées.
        
        Je te laisse jeter un coup d'oeuil à ce qu'il est possible de faire notamment la dernière partie du tutorial :
        http://www.csg.is.titech.ac.jp/~chiba/javassist/tutorial/tut(...)
        Et ici
        http://www.csg.is.titech.ac.jp/~chiba/javassist/tutorial/tut(...)
        Section 5.4 on voit comment il est possible de générer une séquence arbitraire de bytecode.
        
        Bref on a tout ce qu'il faut pour envoyer la JVM dans le mur (même si la bibliothèque étant bien faite, ilf aut quand même y aller)
        
        --
        Kha
        root est un privilège, pas un droit !
        
        [^]Re: C'est trop compliqué !
        
        Posté par Yusei (page perso, ) le 05/01/2008 à 12:25. (lien). Évalué à 2.
        Si une JVM ne donne pas d'interface vers l'extérieur et ne contient pas de failles, alors tu peux générer du bytecode arbitraire, ça ne te permettra pas de faire quoi que ce soit à l'OS derrière la JVM.
        
        Par "pas de code natif", je suppose qu'il voulait interdir l'utilisation de JNI, qui est la principale interface vers l'extérieur de la JVM. Quand tu utilises JNI, tu codes en C (ou équivalent), alors, naturellement, ce n'est pas plus sûr que coder en C. Sans JNI, et en admettant l'utilisation d'une JVM sans failles, je ne pense pas qu'il y ait moyen de faire grand chose.
        
        [^]Re: C'est trop compliqué !
        
        Posté par Jerome Herman () le 05/01/2008 à 12:51. (lien). Évalué à 1.
        Si une JVM ne donne pas d'interface vers l'extérieur et ne contient pas de failles, alors tu peux générer du bytecode arbitraire, ça ne te permettra pas de faire quoi que ce soit à l'OS derrière la JVM.
        
        Bon d'accord je change d'exemple
        
        Même en supposant une JVM aussi parfaite que possible, comme c'est une machine virtuelle basée sur la pile, en lui envoyant le bytecode approprié on peut la forcer à dépiler une information (difficile de surveiller la pile parfaitement quand on est obligée d'interagir avec elle pour le moindre fonctionnement). A partir du moment ou on aura pousser la JVM à dépiler à tort, celle ci aura un comportement inconsistant et peut alors générer toutes les erreurs qu'un programme codé en C avec le pied gauche pourrait générer.
        
        --
        Kha
        root est un privilège, pas un droit !
        
        [^]Re: C'est trop compliqué !
        
        Posté par TImaniac (page perso, ) le 07/01/2008 à 13:52. (lien). Évalué à 1.
        Ben montre moi un programme écrit en Java (pas en bytecode hein) qui permet potentiellement de faire faire n'importe quoi à la JVM sans qu'elle s'en rendre compte.
        Dans tous les cas tu peux admettres que même si une JVM n'est pas une garantie, elle offre une meilleur sécurité. Ce n'est pas certainement pas acceptable si on parle de code mal-intentionné mais c'est toujours bon à prendre pour se protéger de code mal écrit.
        
        --
        MonoFrance
        
        [^]Re: C'est trop compliqué !
        
        Posté par TImaniac (page perso, ) le 07/01/2008 à 13:48. (lien). Évalué à 1.
        mais d'un coté tu dis que les langages de haut niveau sont trop complexes et n'apportent rien
        J'ai écris ca où ? Je n'ai pas généralisé, je parle de Lisaac. En l'occurence je ne vois rien de révolutionnaire en pratique dans ce langage comme a pu l'être la locomotive par rapport à la charette. J'ai pris l'exemple de la sécurité (au sens qualité/bug et au sens protection contre code malveillant), c'est tout.
        
        Choisi ton camps camarade.
        Non. Ce n'est pas le but.
        
        Tout ce que je dis est que du point de vue de l'OS
        Oué c'est pas faux, mamoi j'ai juste rajouté qu'une machine virtuelle qui a un modèle n'offrant d'accès bas niveau comme une JVM ajoute une couche de sécurité en plus de l'OS.
        
        La façon la plus simple de faire celà est d'aller modifier le bytecode d'une des classe de base.
        Tu te rends bien compte que tu triches. Forcement, en java à partir du moment où tu peux écrire dans un fichier tu peux t'amuser à faire écrire à ton programme un Java un bout de code en C ou modifier un fichier de bytecode.
        
        Bref on a tout ce qu'il faut pour envoyer la JVM dans le mur
        Si la JVM est bien faite, tu dois pouvoir la configurer pour interdire au programme exécuter d'intéragir avec les .class du code exécuté. J'avoue ne pas être un spécialiste de la sécu des JVM, mais je suppose qu'une JVM configurée pour exécuter du code provenant du net (style une applet) empêche ce genre d'astuce.
        En tout cas dans l'environnement .NET proche de celui de Java, l'environnement ne laisse pas les composants faire ce genre de connerie s'il ne sont pas de confiance.
        Bref, y'a un modèle "virtuel" intermédiaire avant l'OS qui autorise l'application de tout un ensemple de règles de sécurité plus fines et qui sont toujorus bonnes à prendre avant l'OS.
        Je vois bien une applet écrite en C qui tourne dans un navigateur web. A moins de sandboxer le navigateur dans son ensemble (ce qu'est obligé de faire MS avec IE par exemple), par défaut l'applet C pourrait fai

Journal : Des langages de haut niveau

Plusieurs problèmes avec tes primitves

[^]Re: Plusieurs problèmes avec tes primitves

[^]Re: Plusieurs problèmes avec tes primitves

[^]Re: Plusieurs problèmes avec tes primitves

Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Re: Les trous de lIsaac

[^]Gestion d'erreur lisaac

[^]Re: Gestion d'erreur lisaac

Hein ?

[^]Re: Hein ?

[^]Re: Hein ?

[^]Re: Hein ?

Heu...

C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !

[^]Re: C'est trop compliqué !