Discussion :

[sschneider]

Bonjour,

j'ai un problème avec la syntaxe de B dans un exemple de Atelier B (lien).

Dans la Machine fuel0 ils ont écrit pour l'operation "compute_initial_level":

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

1
2
estimated_level, status :(estimated_level: 0..TANK_CAPACITY & status : tSTATUS & (estimated_level <= WARNING_CAPACITY => status = LOW_LEVEL))

Je comprend le part entre parenthèses, mais pourquoi on dit "estimated_level, status : ( ... )"? L'expression entre parenthèses n'est pas un ensemble?!

Merci beaucoup pour votre aide

[Garulfo]

Ça veut dire qu'on choisit de manière non déterministe les valeurs pour estimated_level et status telles qu'elles vérifient la propritété. Vu que tu as un prédicat, tu as un ensemble par compréhension qui est sous-entendu.

Code :

Sélectionner tout - Visualiser dans une fenêtre à part

v1, v2 : P

revient donc à choisir v1 et v2 tels qu'ils vérifient P.
Une des étapes de raffinement sera de supprimer le non-déterminisme en effectuant un choix précis.

[sschneider]

Ahh... oui j'ai compris le raffinement, c'était seulement l'expression v1,v2 : P que je n'ai pas compris. Ok, c'est clair maintenant.

Merci beaucoup!