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).
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 :-)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker
[^] # Re: Plusieurs problèmes avec tes primitves
Posté par Ontologia (site web personnel) . En réponse au journal Des langages de haut niveau. Évalué à 2.
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 :-)
« Il n’y a pas de choix démocratiques contre les Traités européens » - Jean-Claude Junker