Composing invariants

We explore the question of the composition of invariance specifications in a context of formal methods applied to concurrent and reactive systems. Depending on how compositionality is stated and how invariants are defined, invariance specifications may or m ay not be compositional. This paper examines three classic forms of invariants and their compositional properties. After pointing out what we see as deficiencies of these kinds of invariants, a new fourth form is defined and shown to have useful compositional properties that the more classic forms do not enjoy.