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

*From*: Ron Pressler <r...@xxxxxxxxxxxxxxxxxxx>*Date*: Fri, 12 Feb 2016 02:47:26 -0800 (PST)*References*: <79fff255-1912-451f-8fa7-b671618a3cfe@googlegroups.com> <E7288292-7600-4BF5-8F90-468DDA4C670F@gmail.com>

Hi Stephan.

I'm not sure I follow:

On Friday, February 12, 2016 at 11:30:50 AM UTC+2, Stephan Merz wrote:

On Friday, February 12, 2016 at 11:30:50 AM UTC+2, Stephan Merz wrote:

the soundness of adding auxiliary variables is ensured by the corresponding introduction rules. For example, a simple history variable may be added using a rule such asInit /\ [][Next]_v => \EE h : Init /\ h = h0 /\ [][Next /\ h' = f(h,v) /\ v' # v]_<<v,h>>and the validity of this formula (for arbitrary h0 and f) is proved once and for all.

When you say "arbitrary h0 and f", do you mean for *some* h0 and f (i.e., given h0 and f, this should be proven), or that given a specification, this can be proven for *all* h0 and f (I guess not)? In any event, I can't check this with TLC, right?

In other words, the soundness of auxiliary variables is not checked by TLC but ensured by following syntactic patterns when introducing these variables. There should be a chapter about this in a future version of the Hyperbook.

Do you mean that you have a proof that any mapping is sound if some syntactic patterns are followed? Can we get a sneak-peek at those rules?

Ron

**Follow-Ups**:**Re: [tlaplus] Correctness of refinement mapping***From:*Stephan Merz

**References**:**Correctness of refinement mapping***From:*Ron Pressler

**Re: [tlaplus] Correctness of refinement mapping***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Correctness of refinement mapping** - Next by Date:
**Re: [tlaplus] Correctness of refinement mapping** - Previous by thread:
**Re: [tlaplus] Correctness of refinement mapping** - Next by thread:
**Re: [tlaplus] Correctness of refinement mapping** - Index(es):