Invariants should be Unadorned

Properties that always hold, ie: invariants, should not have to be indicated by special notations.  They should be unadorned.  Special notations should only be used to indicate when a property does not always hold.

Lamport's Temporal Logic of Actions violates this principle in that a predicate P holds only in the initial state, and if you want to indicate that it always holds the you have to put a box symbol in front of it:

[]P

Similarly, in Daniel Jackson's Micromodularity Mechanism you have to use the keyword 'fact' to indicate that a predicate is invariant.

It seems obvious and natural to me that if a predicate P does not always hold then this should be indicated by an implication Q->P where Q is the condition under which P does hold.