Array-Logik (Beispiel mit Quantoren)

(aus Kroening/Strichman, Kap. 7)

Gültigkeit der Invariante x : 0≤x < ia[x] = 0 mathend000# für die Schleife

for (int i = 0; i<N; i++) {
  a[i] = 0;
}
folgt aus Gültigkeit der Formel


    (∀x : (0≤xx < i)⇒select(a, x) = 0)  
  (a' = store(a, i, 0))  
  ...  



2014-03-31