Re: [tlaplus] Utilizing refinement in an inductive proof

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

On 25 Nov 2020, at 18:29, Willy Schultz <will62794@xxxxxxxxx> wrote:

Let's say that I have two specs, SpecWeak and SpecStrong, with next state relations SpecWeakNext and SpecStrongNext, respectively. I have proven that

(T1) SpecStrong => SpecWeak

(T2) SpecWeak /\ []C => []Safety

where C and Safety are some state predicates. That is, SpecStrong is a refinement of SpecWeak, and SpecWeak satisfies Safety under an assumption that []C holds. 

Now, I want to prove that SpecStrong => []C. I can do this by finding an inductive invariant IC such that IC => C. As part of the proof, I will need to prove this inductive step:

(T3) IC /\ SpecStrongNext => IC'

Now, my question is about whether we can re-use (T1) to help prove (T3). Intuitively, it seems that if we assume a "strong induction" approach, then rather than assuming that IC holds only in the current state, we can also assume it held in all states leading the current one. Additionally, we know that every transition we took to get to the current state should have satisfied SpecStrongNext, which, due to (T1), means that each transition also satisfied SpecWeakNext. So, since the finite prefix leading to the current state "satisfies" SpecWeakNext and IC, by (T2) we should be able to assume that Safety held in every state of this prefix, up to and including the current state, allowing us to use Safety in our inductive step i.e.

(T4) IC /\ Safety /\ SpecStrongNext => IC' 

I acknowledge that some of these concepts are not formally defined e.g. usually we only talk about infinite traces "satisfying" a temporal formula. The intuition seems sound, though. I'm curious if there's a better formalization of this technique or precedent for this kind of proof structure.

--
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/ed95f750-1b69-4b30-8f41-567a7081848bn%40googlegroups.com.

--
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.