`@@ -7,28 +7,38 @@
`` `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 ~~such a ~~
shadows...

`+`!! 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:

` `

`-`~~Let ~~
_m_ a ~~method containing a shadow ~~
_~~s~~
_ ~~in ~~
_~~initShadows(~~
A~~)~~
_ ~~for some tracematch automaton ~~
_A_.

`+`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 _~~cinit~~
_ ~~the initial ~~
(~~dynamic~~
) ~~configuration of ~~
A.

`+`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_, ..., 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:

`-`_m_ is dynamically _A_-invariant w.r.t. _s_ if on every ~~finite path (s0,...,sn) through ~~
_~~m~~
_ ~~starting at ~~
_~~s~~
_ ~~(i.e. s0 = "stmt at _s_") it holds that ~~
dynamicConfiguration(sn)=_cinit_.

`+`method
_m_ is dynamically _A_-invariant w.r.t. shadow
_s_ if on every execution
_e
_ in
_E
_,
dynamicConfiguration(sn)=_cinit_.

` `</b>

` `

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

` `

`-`Let _m_ a method containing a shadow _s_ in _initShadows(A)_ for some tracematch automaton _A_.

`+`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_, ..., s_n) through _m_ starting at the program point corresponding to the shadow _s_ and ending with a return from _m
_.

`-`Let _cinit_ the initial (static) configuration of A.

`+`Let _cinit_ be
the initial (static) configuration of A.

`-`_m_ is statically _A_-invariant w.r.t. _s_ if on every ~~finite path (s0,...,sn) through ~~
_~~m~~
_ ~~starting at ~~
_~~s~~
_ ~~(i.e. s0 = "stmt at _s_") it holds that ~~
staticConfiguration(sn)=_cinit_.

`+`_m_ is statically _A_-invariant w.r.t. _s_ if on every execution
_e
_ in
_E
_,
staticConfiguration(sn)=_cinit_.