Array-Logik (Beispiel mit Quantoren)

(aus Kroening/Strichman, Kap. 7)

Gültigkeit der Invariante ∀x : 0≤x < i⇒a[x] = 0 mathend000# für die Schleife

for (int i = 0; i<N; i++) {
  a[i] = 0;
}

folgt aus Gültigkeit der Formel

∧ (a' = store(a, i, 0))

⇒ ...