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 pointed out in [2], an algorithm's transition behavior depends only on the current state, not on its history of states, 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.