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

[Changgeng Zhao]

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? 

[Stephan Merz]

Hello,

I have a hard time understanding the question. For one thing, the parameter a of subaction1 appears to be a variable (since you use a') but in subaction2 the quantified variable a denotes a value, and therefore a' = a.

Also, when you write a specification that involves sets of values, you typically use functions and have actions with conjuncts of the form

  x' = [x EXCEPT ![a] = ...]

Then, if you try to combine several of those you obtain

  \A a \in A : x' = [x EXCEPT ![a] = ...]

which is contradictory when A has more than one element.

Perhaps you could share a more complete specification to clarify what you are trying to achieve.

Regards,

Stephan

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 doesn't have same behavior? 

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

[Changgeng Zhao]

OK, let me show it in another way. 

Suppose I have one higher level specification:

  VARIABLE a      \* a is an integer

  Next == \/ otherSubActions

               \/ a' = a + 1

And now I want to design a implementation which refines the above specification, but in the implementation it batches the a' = a + 1 steps:

  VARIABLE a       \* a is an integer

  Next == \/ otherSubActions

               \/ a' = a + 10

In the implementation the variable "a" always increases 10 at a time, which means batching 10 steps of the specification's subAction2.

I think this is actually a kind of refinement,  but I can not use stuttering variables to prove it, because : after each step of Specification, the variable "a" will change, while stuttering steps don't change any external state.

[Leslie Lamport]

You write that "I think this is actually a kind of refinement but I
can not ...  prove it".  I can't tell you how to prove that something
is "a kind of refinement" without knowing precisely what that means.
However, let me point out first that your "higher-level specification"
implements your "implementation" under the refinement mapping

   a <- 10 * (a \div 10)

(Note that 10 * (a \div 10) is the largest multiple of 10
that is =< a.)

If you add a stuttering variable v to your "implementation" that
adds 9 steps that leave a unchanged between each change to a,
it will be easy to show that this new spec implements your
"higher-level specification" under a refinement mapping

   a <- some expression in v and a

Leslie

[Changgeng Zhao]

Hi Leslie,

Thank you for your promote reply and suggestion which exactly solved my confusions!

Now I understand how to do the mapping by adding stuttering variables and I will try my best to make my words precise from now on.

Changgeng