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

*From*: Changgeng Zhao <zcg...@xxxxxxxxx>*Date*: Thu, 22 Mar 2018 20:35:08 -0700 (PDT)

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?

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

**Re: [tlaplus] How to give a refinement mapping from one subactions to many subactions***From:*Stephan Merz

- Prev by Date:
**TLA+ Community Meeting** - Next by Date:
**Re: [tlaplus] How to give a refinement mapping from one subactions to many subactions** - Previous by thread:
**Re: [tlaplus] Re: TLA+ Community Meeting** - Next by thread:
**Re: [tlaplus] How to give a refinement mapping from one subactions to many subactions** - Index(es):