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

*From*: Willy Schultz <will62794@xxxxxxxxx>*Date*: Sun, 13 Sep 2020 12:53:41 -0700 (PDT)

My understanding is that it should always be possible to prove a safety property of a specification by finding an inductive invariant [1]. For safety properties that can be expressed as state predicates (i.e. invariants), the technique is clear to me i.e. find an inductive invariant, prove that it holds in the initial state and prove the inductive step. There are some safety properties, however, that cannot be expressed as state predicates. For example, a property such as "x=1 at most once" is a safety property, since it will be violated at a discrete point in the behavior, but its truth value depends on a behavior prefix rather than a single state.

My question is about how one should go about proving a safety property of this form i.e. a safety property that is not a "state invariance" property, but a "prefix invariance" (for lack of a better term) property. I have worked on one specification where I encountered this issue, and it's easy enough to use history variables in that case to remedy the problem. That is, maintain a history variable that stores enough information about the previous states of the current behavior so that a "prefix invariance" property can be expressed as a state predicate on the appropriate history variables. Here's a simple example of using history variables to illustrate the "x=1 at most once" example. (As a possibly related aside, I was also unable to figure out a way to express a property like "x=1 at most once" in TLA+ without using a history variable.)

------------ MODULE history -----------------

EXTENDS Naturals, Sequences

VARIABLE x, xHist

Init ==

/\ x = 0

/\ xHist = <<>>

Next ==

/\ x < 2

/\ x' = x + 1

/\ xHist' = Append(xHist, x+1)

\* Safety property: x = 1 at most once.

Inv == ~(\E i,j \in DOMAIN xHist : i # j /\ xHist[i] = 1 /\ xHist[j] = 1)

==============================================

From a practical standpoint, this seems to work fine, but I'm curious if there are alternative proof techniques to deal with safety properties of this type. I am slightly confused by the fact that an inductive proof would necessarily require history variables. As Lamport points out, an algorithm's transition behavior depends only on the current state, not on its history of states [2], so if a safety property can be proved by an inductive invariant, it seems like history variables shouldn't be fundamentally needed, since the algorithm itself doesn't have access to these history variables, and yet it manages to uphold the invariant.

[1] https://lamport.azurewebsites.net/tla/proving-safety.pdf

[2] https://lamport.azurewebsites.net/pubs/teaching-concurrency.pdf

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/91ccc7aa-6a12-4e46-84e0-54c5282d39een%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Proving Prefix Safety Properties***From:*Willy Schultz

**Re: [tlaplus] Proving Prefix Safety Properties***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)** - Next by Date:
**[tlaplus] Java overflow when using RandomSubset to check inductive invariance** - Previous by thread:
**[tlaplus] Re: Using formal methods to reason about probabilistic systems** - Next by thread:
**Re: [tlaplus] Proving Prefix Safety Properties** - Index(es):