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

*From*: Stephan Merz <stephan.merz@xxxxxxxxx>*Date*: Wed, 25 Nov 2020 18:50:15 +0100*References*: <ed95f750-1b69-4b30-8f41-567a7081848bn@googlegroups.com>

I don't really understand in which sense you say that your proposed approach reuses (T1) since SpecWeak (or its next-state relation) doesn't occur in T4. It sounds to me that really your inductive invariant should be IC /\ Safety By (T4) it remains to prove IC /\ Safety /\ SpecStrongNext => Safety' Now, assuming that the proof of (T2) is a standard invariance proof, it will include a step Safety /\ C /\ C' /\ SpecWeakNext => Safety' and if we also have SpecStrongNext => SpecWeakNext then we are done, using the fact that IC => C. If however for proving (T1), you needed an additional invariant, you'd want to conjoin that predicate to IC /\ Safety. Stephan
--
You received this message because you are subscribed to the Google Groups "tlaplus" group. To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx. To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/FFB7E75E-1ED9-40A2-B8DF-821CEAB201EF%40gmail.com. |

**References**:**[tlaplus] Utilizing refinement in an inductive proof***From:*Willy Schultz

- Prev by Date:
**[tlaplus] Utilizing refinement in an inductive proof** - Next by Date:
**Re: [tlaplus] Canonical TLA+ ... how to avoid "imperative brainwash" on KV store** - Previous by thread:
**[tlaplus] Utilizing refinement in an inductive proof** - Next by thread:
**[tlaplus] Specifying an arbitrary function and then using it in TLC** - Index(es):