%
small theory of transition relations transitions [states: TYPE+, INIT: pred[states], REL: pred [ [states, states] ] ]: THEORY BEGIN % To prove that a property P is an invariant, we prove it is *inductive* % This is similar to Amir Pnueli's rule for Universal Invariance % Except that we strengthen the actual property rather than have an auxiliary indinv(P: pred[states]): bool = (FORALL (s: states): INIT(s) => P(s)) AND (FORALL (pre, post: states): P(pre) AND REL(pre, post) => P(post)) s, t: VAR states REACHABLE(s): INDUCTIVE bool = INIT(s) OR (EXISTS t: REACHABLE(t) AND REL(t,s)) P: VAR pred[states] invariant(P): bool = FORALL s: REACHABLE(s) => P(s) indinv_is_invariant: LEMMA indinv(P) => invariant(P) invariant_closed_on_reachable: LEMMA invariant(P) => FORALL t: (EXISTS s: REACHABLE(s) AND P(s) AND REL(s, t)) => P(t) END transitions