\begin{slide}{Array-Logik (Beispiel mit Quantoren)}

(aus Kroening/Strichman, Kap. 7)

Gültigkeit der Invariante 
\( \forall x: 0\le x< i \Rightarrow 
a[x]=0
\)
für die Schleife
\begin{verbatim}
for (int i = 0; i<N; i++) {
  a[i] = 0;
}
\end{verbatim}
folgt aus Gültigkeit der Formel

\begin{eqnarray*}
&& (\forall x: (0\le x\wedge x < i) 
\Rightarrow \select(a,x)=0 )\\
&\wedge& (a' = \store(a,i,0)) \\
&\Rightarrow& \dots
\end{eqnarray*}

\end{slide}

\begin{slide}{Array-Logik (Beispiel QF\_AX)}

\begin{verbatim}
(set-logic QF_AX)
(declare-sort Index 0) 
(declare-sort Element 0) 
(declare-fun a () (Array Index Element)) 
(declare-fun i () Index) 
(declare-fun x () Element) 
(declare-fun y () Element) 
(assert (not (= (store (store a i x) i y)
                (store a i y))))
(check-sat)
\end{verbatim}

\end{slide}

\begin{slide}{Array-Logik (Beispiel QF\_AUFLIA)}

\begin{verbatim}
(set-logic QF_AUFLIA)
(declare-fun a () (Array Int Int)) 
(declare-fun b () (Array Int Int)) 
(declare-fun i () Int) 
(declare-fun j () Int) 
(declare-fun k () Int) 
(assert (< i j))
(assert (< (select a i) (select a j)))
(assert (= b (store a k 0)))
(assert (> i k))
(assert (> (select b i) (select b j)))
(check-sat)
\end{verbatim}

\end{slide}
