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

How to give a refinement mapping from one subactions to many subactions



I am trying to prove one algorithm refines another algorithm. Let's call them Implementation and Specification. 

For example, the Specification has one subaction that :

subaction1(a) == /\ F1(a)
                            /\ F2(a')

While in the Implementation, it will batch several of this step in one subaction, which is like:

subaction2(A) == 
    \A a \in A : 
        /\ F1(a) /\ F2(a')

(A is a set consisting of element a, and each element doesn't interfere with other elements in A)

Then how can I represent it with the format of refinement mapping, for example using auxiliary variables? Or is it not a refinement mapping cause they don't have same behaviors?