Discussion :

[Tiéry]

Bonjour je fais actuellement du B dans le cadre de mes études et j'utilise l'atelier B4free, je voudrais juste un renseignement:

La doc parle d'un fichier exec contenant les sources (C ou ADA) généré par l'atelier pour une machine or ce fichier est vide chez moi, y a til une commande a tapez pour généré ces sources

[DavidDeharbe]

Bonjour je fais actuellement du B dans le cadre de mes études et j'utilise l'atelier B4free, je voudrais juste un renseignement:

La doc parle d'un fichier exec contenant les sources (C ou ADA) généré par l'atelier pour une machine or ce fichier est vide chez moi, y a til une commande a tapez pour généré ces sources

Je pense que la synthese de code C et ADA est une option reservee a la version commerciale et payante: Atelier B (www.atelierb.societe.com).

Je crois bien que l'outil JBTools permet la synthese de code Java et C#, mais je ne l'ai jamais utilise personnellement.

David.
--

[Tiéry]

Merci, je n'ai pas trouver de réponse meme avec la version payante, cependant il semblerai qu'il faudrait faire plusieurs raffinement pour aboutir a une verion plus concrete (et donc obtenir le code c ou ada), ma machine ne l'était tout simplment pas assez


mais je m'en fout les axams sont fini et je suis en vacances

[DavidDeharbe]

Merci, je n'ai pas trouver de réponse meme avec la version payante, cependant il semblerai qu'il faudrait faire plusieurs raffinement pour aboutir a une verion plus concrete (et donc obtenir le code c ou ada), ma machine ne l'était tout simplment pas assez


mais je m'en fout les axams sont fini et je suis en vacances

Effectivement, les outils ne sont pas capables de synthétiser n'importe quelle opération B. Par exemple le non-déterminisme doit être éliminé (par raffinement) avant de passer à la synthèse. Il existe d'autres contraintes, documentées.

Bonnes vacances...

David.
--

[ThierryLecomte]

B4Free est une version light de l'Atelier B pour s'initier à la modélisation en B et à la preuve. Toutes les fonctionnalités sont actives mais il faut noter quelques restrictions:
- pas de générateur de code (B4Free et Atelier B partagent la même documentation).
- pas de support du multi-utilisateur.
- nombre d'obligations de preuve limité à 1000 par composants.