| Hi Ron,
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 as
Init /\ [][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?
there is nothing to prove: the right-hand side corresponds to an inductive definition of a primitive-recursive function where the initial value of h is h0 and at every step, the new value of h is computed as a function of the visible variables v and the previous value of h. (To be completely precise, I'm assuming that h does not occur in Init, Next or h0 and that h' does not occur in f(h,v).) In any event, I can't check this with TLC, right?
No, TLC cannot check this. (We expect TLAPS to be eventually able to prove such formulas but we first have to support standard first-order logic before we think about quantification.)
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?
I'll send you a rough draft off-list.
Stephan
|