SableWiki - Diff: Formal Definition of Invariant Methods

Differences between current version and predecessor to the previous major change of Formal Definition of Invariant Methods.

Other diffs: Previous Revision, Previous Author

Newer page: version 6 Last edited on February 23, 2007 3:09 pm. by PatrickLam
Older page: version 3 Last edited on February 23, 2007 10:39 am. by EricBodden
@@ -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:  
 <b> 
-_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. 
  
+Then:  
 <b> 
-_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_. 
 </b> 
  
 !! Theorem