[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Verifying refinement

Hi there,

Suppose we have two modules and one module should be the refinement of the other one (let's call them module Simple and module Implementation). Module Simple has one action that is split into two actions within module Implementation. For example

SimpleAction ==
    /\ var1' = value1
    /\ var2' = value2

SplitAction1 ==
    /\ var1' = value1
    /\ UNCHANGED var2

SplitAction2 ==
    /\ var2' = value2
    /\UNCHANGED var1

When I try to check "Simple!Spec" would it produce an error trace? Since in module Simple, there are no actions that change the values of "var1" and "var2" separately. Is it incorrect thinking that module Implementation is a refinement of module  Simple? I mean, in this situation am I conceptually wrong about refinement? Thanks!


Pedro Yuri Arbs Paiva
Engenheiro Eletrônico
Instituto Tecnológico de Aeronáutica (T-16)
(+55) 12 98106-4129