« Young Adolph by Beryl Bainbridge | Main | The Periodic Table by Primo Levi »

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:


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. 

Reader Comments

There are no comments for this journal entry. To create a new comment, use the form below.

PostPost a New Comment

Enter your information below to add a new comment.
Author Email (optional):
Author URL (optional):
All HTML will be escaped. Hyperlinks will be created for URLs automatically.