First we look for all shadows triggering an "initial edge" in the TM automaton...

Let A=(Q,q_0,A,E,F) a tracematch automaton.

Let initEdges(A) = { (q_0,a,q) in E | q in Q }.

Let initLabels(A)= { a | (q,a,p) in initEdges(A) }.

Let initShadows(A) = { s in Shadows | label(s) in initLabels(A)}.

Then, we define invariance (only!) for methods with initial shadows...

We will define the notions of dynamic and static invariance. These differ in that dynamic invariance leaves the dynamic configuration of the automaton unchanged, whereas static invariance leaves the static approximation of the automaton's configuration unchanged. Note that both dynamic and static invariance are properties that must hold on all executions of the method.

Dynamic automata differ from static automata as follows: dynamic automata contain the references to heap objects, while static contain references to some abstraction of these heap objects, typically points-to sets.

First "dynamic" invariance:

Conceptually, method m is dynamically invariant for a automaton A when running any execution e starting from A's initial configuration leaves A in the initial configuration at the end of e.

Let m be a method containing a shadow s in initShadows(A) for some tracematch automaton A. Let E be the set of executions of method s, i.e. the finite paths (s_0, ..., s_n) through m starting at the program point corresponding to the shadow s and ending with a return from m.

Let cinit be the initial (dynamic) configuration of A.

Then: method m is dynamically A-invariant w.r.t. shadow s if on every execution e in E, dynamicConfiguration(sn)=cinit.

Now "static invariance" (quite similar) ...

Informally, a method m is statically invariant for an automaton A if running any execution e starting from the static representation of A's initial configuration leaves the static representation of A in its initial configuration at the end of e.

Let m be a method containing a shadow s in initShadows(A) for some tracematch automaton A. Let E be the set of executions of method s, i.e. the finite paths (s_0, ..., s_n) through m starting at the program point corresponding to the shadow s and ending with a return from m.

Let cinit be the initial (static) configuration of A.

Then: m is statically A-invariant w.r.t. s if on every execution e in E, staticConfiguration(sn)=cinit.

Theorem

If the static configurations of A represent a sound over-approximation (what that is, we still have to define) of the dynamic configurations of A then it follows that for each pair (m, s) of a method m and an init shadow s in m: if m is statically A-invariant w.r.t. s then m is also dynamically A-invariant w.r.t. s.

Proof

If the static configurations of A represent a sound over-approximation, then for each pair (st, dy) of static and related dynamic configuration and for each state q in Q it holds that the disjuncts of q in st are a superset of the disjuncts of q in dy. Consequently, at each tail statement of m, if staticConfiguration(sn)=cinit = (true,false,...,false) then dynamicConfiguration(sn)=cinit must also hold. q.e.d.