Raffinement d'une spécification B

Considérez que je donne les résultats suivants dans la spécification B: -Raffinement d'une spécification B

flower <: FLOWER 
age <: AGE 
owner <: OWNER 
Type <: flower * age 
Buyer : owner <-> flower

moi Est-il possible de créer un raffinement comme suit: -

flower <: FLOWER 
age <: AGE 
owner <: OWNER 
Type : Owner <-> flower * age 
Buyer : owner <-> flower

Source

2017-07-19 user1797730

Quelle est la question? – drum

les deux ne savent pas ce que vous demandez et apparemment hors-sujet (https://math.stackexchange.com/ peut-être) –

@RachelGallen: Je pense que la question est sur le sujet parce que la méthode B est une méthode de développement de logiciels et ici même le code concret est montré. – danielp

Non, ce n'est pas possible parce que dans un raffinement le type d'une variable doit avoir le même type que dans la spécification (s'il y a une variable avec le même nom dans la spécification comme ici).

Source

2017-07-20 07:13:05 danielp

Raffinement d'une spécification B

Répondre

Questions connexes