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)*}.

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.

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.
**

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.
**

**
If the static configurations of A represent a sound over-approximation **(what that is, we still have to define)

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.*