As it is stated in the UNITY book (page 49):
"If x = y is an invariant of program F, x can replace y in all properties of F. (...) A particularly useful form of this axiom is to replace true by an invariant I, and vice versa."
The idea is that, if I is an invariant of F, then it is always true in F, i.e., true in any state of any computation of F. Therefore, I can be replaced by true anywhere it appears in properties without changing the truth of these properties.
In UNITY, a predicate I is invariant in program F iff:
Obviously, if a predicate is invariant, it is always true (by induction, it is true in the beginning and cannot be falsified). However, the converse is not true: A predicate can be always true in any state of any computation of a program and not be an invariant of that program.
The reason is that some states may not be reachable, i.e., they do not appear in any computation of the program. A triple like {p} s {q} does not take reachable states into account: If a state satisfies p and statement s is executed from that state, the resulting state must satisfy q, whether the starting state is reachable or not. Now, if a predicate I can be falsified by some statements only when they are executed from a nonreachable state, I is not an invariant (from the definition of invariant). But it can still be always true in any reachable state of the program.
The following figure illustrates the situation when a predicate p is always true but is not an invariant.
The green zone is the set of all possible states; the blue zone is the set of all reachable states; the red zone represents a predicate p.
The predicate p is clearly always true (since all the reachable states are included in p). A transition starting in a reachable state must stay in a reachable state, from the definition of a reachable state (type "a" transitions). However, a transition starting in a nonreachable state that satisfies p may end in a state that does not satisfy p (type "d" transitions). If such a transition exists, then p is always true, but is not an invariant.
If SI is the predicate that corresponds to the blue zone of reachable states (SI is often called the strongest invariant because... well, it is!), then, because transitions cannot escape the blue zone, SI is an invariant. So is SI /\ p, because SI /\ p = SI. Using the substitution axiom, we can replace SI by true and deduce that p is an invariant, which is not necessarily the case (p is only always true). Hence the consistency problem in UNITY logic.
In other words, UNITY logic, without the substitution axiom, allows us to prove invariant properties. With the substitution axiom, it allows us to prove always true properties. Since always true properties and invariant properties do not coincide, the logic is inconsistent.
In her paper, Beverly Sanders defines formally the "always true" properties as well as the predicate SI. The resulting logic, which only deals with always true properties and does not care about invariants, is then consistent. Unfortunately, she kept calling those properties invariant, which has led to a lot of confusion.
However, it appears that both invariants and always true properties are interesting. It is rather obvious that always true properties are interesting (we like to know what is true when a program is running), but invariants are also of interest (see, for instance, the problem of mechanical verification, or the problem of composition).
Therefore, it seems that a logic should keep those two families of properties using, of course, a different name for each family. Personnaly, I like "invariant" and "always true". The usage, in the world of temporal logic, is more to use "invariant" (to refer to always true properties) and "inductive invariant" (to refer to (what I call) invariant properties). Confusing, no? To avoid any ambiguity, one can always (invariantly?) talk of "inductive invariants" and "noninductive always true properties", but it's rather inconvenient...
>
Last modified: Fri Feb 11 11:11:38 EST 2000