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

[Changgeng Zhao <zcg...@xxxxxxxxx>]

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

On Wednesday, March 28, 2018 at 6:13:55 AM UTC+8, Leslie Lamport wrote:

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

On Thursday, March 22, 2018 at 8:33:23 PM UTC-7, Changgeng Zhao wrote:

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?