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

*From*: Changgeng Zhao <zcg...@xxxxxxxxx>*Date*: Tue, 27 Mar 2018 20:41:41 -0700 (PDT)*References*: <c2c1a8ae-df92-458c-8100-9626eac2f23b@googlegroups.com> <a6cee473-623c-4f5b-be79-f261ce98436c@googlegroups.com>

Hi Leslie,

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 mappinga <- 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 mappinga <- some _expression_ in v and aLeslie

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?

**References**:**How to give a refinement mapping from one subactions to many subactions***From:*Changgeng Zhao

**Re: How to give a refinement mapping from one subactions to many subactions***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] relevant conferences?** - Next by Date:
**How do I create a TLC model for a specific module in a spec with the toolbox?** - Previous by thread:
**Re: How to give a refinement mapping from one subactions to many subactions** - Next by thread:
**Fairness condition for messages** - Index(es):