Discussion :

[nana2020]

Bonsoir,
est ce qu'on peut utilisé la methode B et l'atelier B pour la verification des applications ecrit dans un autre langage ( C , java,............)
ou bien
la methode B est utilisé dans la reailisation d 'un verifieur ?
autre chose :
comment on peut passé de B vers un code C ou ada ......
merci .

[Garulfo]

Bonsoir,
est ce qu'on peut utilisé la methode B et l'atelier B pour la verification des applications ecrit dans un autre langage ( C , java,............)

On ne peut pas vérifier a posteriori une application à partir de la méthode B du moins sans un énorme travail d'amont (modélisation du C en B). Ce n'est pas du tout le but de cette méthode.

la methode B est utilisé dans la reailisation d 'un verifieur ?

Je ne comprends pas la deuxième question.

Bonsoir,
comment on peut passé de B vers un code C ou ada ......

À l'aide d'un traducteur. Pour cela il faut la version payante (et très cher) de l'Atelier B. La version académique est dénué de cette fonction je crois me rappeler.

Ça serait sympa de rédiger des messages dans un français correct merci.

[sschneider]

À l'aide d'un traducteur. Pour cela il faut la version payante (et très cher) de l'Atelier B. La version académique est dénué de cette fonction je crois me rappeler.

Bonjour,

version 4.0 de l'Atelier B contient ComenC (et c'est gratuit )
ComenC peut passer de B vers C.

[Garulfo]

Bonjour,

version 4.0 de l'Atelier B contient ComenC (et c'est gratuit )
ComenC peut passer de B vers C.

Ah c'est bien possible. Depuis j'ai un peu basculé vers Event-B. Ce qui fait que je n'ai pas suivi les nouveautés de l'Atelier B 4.0
TOujours bon à savoir.