Lab for Automated Reasoning and Analysis LARA

Space of Invariants

Problem Statement

Let $S$ be a set (e.g. the set of all integers). Let $\textit{Init}, \textit{Good} \subseteq S$ and $r \subseteq S \times S$. Define

\begin{equation*}
   \textit{Invs} = \{ I \subseteq S \mid \textit{Init} \subseteq I \land sp(I,r)\subseteq I \land I \subseteq \textit{Good} \}
\end{equation*}

For each element $I \in \textit{Invs}$ we have $I \subseteq S$ and we think of $I$ as an invariant.

Prove each of the following statements or give a counterexample.

a): If $\textit{Invs} \neq \emptyset$, then $sp(\textit{Init},r^*) \subseteq \textit{Good}$.

b): The set $\textit{Invs}$ is finite.

c): If $I_1,I_2 \in \textit{Invs}$ then also $I_1 \cup I_2 \in \textit{Invs}$.

d): If $I_1,I_2 \in \textit{Invs}$ then also $I_1 \cap I_2 \in \textit{Invs}$.

e): Let $\textit{Invs}1 \subseteq \textit{Invs}$ and let

\begin{equation*}
    J = \bigcap_{I \in \textit{Invs}1} I
\end{equation*}

in other words, by definition of $\bigcap$,

\begin{equation*}
   J = \{ x \mid \forall I \in \textit{Invs}1.\ x \in I \}
\end{equation*}

Prove that then $J \in \textit{Invs}$. What do we obtain for $\textit{Invs}1 = \textit{Invs}$?

f): Let $\textit{Invs}1 \subseteq \textit{Invs}$ and let

\begin{equation*}
    K = \bigcup_{I \in \textit{Invs}1} I
\end{equation*}

in other words, by definition of $\bigcup$,

\begin{equation*}
    K = \{ x \mid \exists I \in \textit{Invs}1.\ x \in I \}
\end{equation*}

Prove that then $K \in \textit{Invs}$. What do we obtain for $\textit{Invs}1 = \textit{Invs}$?

g): Is the set $Invs$ a lattice? If it is a lattice, is it complete? If it is not a lattice, can it be modified to become a lattice?

Solutions

Solution a)

True.

First we prove the following lemme using induction on $n$.


Lemma

\begin{equation*}
 \forall I\in\textit{Invs}.\forall n\in\mathbb{N}. sp(\textit{Init},\bigcup_{i = 0}^{n} r^i)\subseteq I
\end{equation*}

Base. Assume $n = 0$.

We show $\forall I\in\textit{Invs}.sp(\it{Init},r^0)\subseteq I$.

\begin{equation*}
\begin{align}
\forall I\in\textit{Invs}.sp(\it{Init},r^0)\subseteq I &\Longleftrightarrow \forall I\in\textit{Invs}.sp(\it{Init},\Delta_S)\subseteq I\\
&\Longleftrightarrow \forall I\in\textit{Invs}. \it{Init}\subseteq I
\end{align}
\end{equation*}

This holds according to the definition of invariants.

Inductive step. Assume $\forall I\in\textit{Invs}.sp(\textit{Init},\bigcup_{i = 0}^{n} r^i)\subseteq I$. We show $\forall I\in\textit{Invs}.sp(\textit{Init},\bigcup_{i = 0}^{n+1} r^i)\subseteq I$.

\begin{equation*}
\begin{align}
\forall I\in\textit{Invs}.sp(\textit{Init},\bigcup_{i = 0}^{n+1} r^i)\subseteq I
&\Longleftrightarrow \forall I\in\textit{Invs}.sp(\it{Init},\bigcup_{i = 0}^{n} r^i\cup r^{n+1})\subseteq I \\
\mbox{By disjunctivity of sp,}\\
&\Longleftrightarrow \forall I\in\textit{Invs}.(sp(\it{Init},\bigcup_{i = 0}^{n} r^i) \cup sp(\it{Init},r^{n+1}))\subseteq I \\
&\Longleftrightarrow (\forall I\in\textit{Invs}.sp(\it{Init},\bigcup_{i = 0}^{n} r^i)\subseteq I)\wedge (\forall I\in\textit{Invs}.sp(\it{Init},r^{n+1})\subseteq I) \\
\mbox{By the induction assumption,}\\
&\Longrightarrow \forall I\in\textit{Invs}.sp(\it{Init},r^{n+1})\subseteq I\\
&\Longleftrightarrow \forall I\in\textit{Invs}.sp(\it{Init},r^{n} \circ r)\subseteq I\\
&\Longleftrightarrow \forall I\in\textit{Invs}.sp(sp(\it{Init},r^{n}),r)\subseteq I
\end{align}
\end{equation*}

By the induction assumption we know $\forall I\in\textit{Invs}.sp(\textit{Init},\bigcup_{i = 0}^{n} r^i)\subseteq I$.

We can easily show for two invariants $I$ and $I_1$ that $I\in \textit{Invs}\wedge I_1\subseteq I\Longrightarrow sp(I_1,r)\subseteq I$. This proves the lemma.


From the lemma we can conclude $\forall I\in\textit{Invs}. sp(\textit{Init},r^{*})\subseteq I$.

The set $\textit{Invs}$ is non-empty, so there exists $I_1$ such that $\it{Init}\subseteq I_1\wedge sp(I_1,r)\subseteq I_1 \land I_1\subseteq \textit{Good}$. This shows that $sp(\textit{Init},r^{*})\subseteq\textit{Good}$.

Solution b)

False.

You can easily find counter-examples.

Solution c,d)

Both true.

The assumption $I_1, I_2\in \textit{Invs}$ gives us the following.

\begin{equation*}
\begin{align}
 &\it{Init}\subseteq I_1\wedge sp(I_1,r)\subseteq I_1 \land I_1\subseteq \textit{Good}  \   \bigwedge\\
 &\it{Init}\subseteq I_2\wedge sp(I_2,r)\subseteq I_2 \land I_2\subseteq \textit{Good} 
\end{align}
\end{equation*}

From the set theory we know that if $A\subseteq B$ and $C\subseteq D$ then we can conclude both $A\cup C\subseteq B\cup D$ and $A\cap C\subseteq B\cap D$.

We can use this fact on the on the corresponding components:

$\it{Init}\subseteq I_1 \wedge  sp(I_1,r)\subseteq I_1   \wedge  I_1\subseteq \textit{Good}  \bigwedge$
$\cup\updownarrow\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \cup}\updownarrow\mbox{ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \cup}\updownarrow$
$\it{Init}\subseteq I_2 \wedge sp(I_2,r)\subseteq I_2 \wedge I_2\subseteq \textit{Good}$

Computing the union gives us:

\begin{equation*}
 (\it{Init}\subseteq I_1\cup I_2) \wedge (sp(I_1,r)\cup sp(I_2,r)\subseteq I_1\cup I_2) \wedge (I_1\cup I_2\subseteq \textit{Good})
\end{equation*}

Due of the disjunctivity of $sp$ we can conclude that $I_1\cup I_2$ is an invariant.

For the intersection case we replace the invariant of $sp(I_1,r)\subseteq I_1$ with a stronger one $sp(I_1\cap I_2,r)\subseteq I_1$. Similarly for $sp(I_2,r)\subseteq I_2$.

This can be done due to the monotonicity of $sp$.

$\it{Init}\subseteq I_1 \wedge sp(I_1\cap I_2,r)\subseteq I_1 \wedge I_1\subseteq \textit{Good} \bigwedge$
$\cap\updownarrow\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \cap}\updownarrow\mbox{\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \cap}\updownarrow$
$\it{Init}\subseteq I_2 \wedge sp(I_1\cap I_2,r)\subseteq I_2 \wedge I_2\subseteq \textit{Good}$

The proof is similar to the union case.

Solution e)

Consider the following equivalence.

\begin{equation*}
 J\in \textit{Invs}\Longleftrightarrow (\it{Init}\subseteq J \wedge sp(J,r)\subseteq J\wedge J\subseteq \textit{Good})
\end{equation*}

We show that each conjunct is valid.

  • $\it{Init}\subseteq J$. Holds since $\it{Init}$ is included in every invariant.
  • $sp(J,r)\subseteq J$

Let $x$ be an arbitrary member of $sp(J,r)$.

\begin{equation*}
\begin{align}
x\in sp(J,r) &\Longleftrightarrow \exists y. y\in J\wedge(y,x)\in r \\
&\Longleftrightarrow \exists y.(\forall I\in \textit{Invs}1.y\in I)\wedge(y,x)\in r \\
\end{align}
\end{equation*}

Nested quantifiers can be swapped, but the reverse does not necessarily hold.

\begin{equation*}
\begin{align}
&\Longrightarrow \forall I\in\textit{Invs}1.\exists y.y\in I\wedge(y,x)\in r\\
&\Longleftrightarrow \forall I\in\textit{Invs}1.x\in sp(I,r)\\
\mbox{Since $I$ is an invariant,}\\
&\Longrightarrow \forall I\in\textit{Invs}1.x\in I\\
&\Longleftrightarrow x\in J\\
\end{align}
\end{equation*}

  • $J\subseteq \textit{Good}$. Holds if $\textit{Invs}$ is non-empty.

If $\textit{Invs} \neq\emptyset$ and $\textit{Invs}1 = \textit{Invs}$ we claim $J = sp(\textit{Init},r^*)$.

We proved in (a) that $sp(\textit{Init},r^*) \subseteq \textit{Good}$. It remains to prove the other two conditions.

  • $\it{Init}\subseteq sp(\it{Init},r^{*})$

\begin{equation*}
\begin{align}
sp(\it{Init},r^{*}) &= sp(\it{Init},r^{*}\cup\Delta_S)\\
&= sp(\it{Init},r^{*})\cup sp(\it{Init},\Delta_S)\\
&= sp(\it{Init},r^{*})\cup \it{Init}
\end{align}
\end{equation*}

Which shows that $\it{Init}$ is included in $sp(\it{Init},r^{*})$.

  • $sp(sp(\it{Init},r^{*}),r)\subseteq sp(\it{Init},r^{*})$

This is correct because $sp(\it{Init},r^{*}) = sp(\it{Init},r^{*}\circ r)\cup\Delta_S$

To prove that $sp(\textit{Init},r^*)$ is the bottom element we have to prove the following.

\begin{equation*}
 \forall I\in\it{Invs}. sp(\it{Init},r^*)\subseteq I
\end{equation*}

Which was proved in a lemma in part (a).

Solution f)

Consider the following equivalence.

\begin{equation*}
 K\in \textit{Invs}\Longleftrightarrow (\it{Init}\subseteq K \wedge sp(K,r)\subseteq K\wedge K\subseteq \textit{Good})
\end{equation*}

We show that each conjunct is valid.

  • $\it{Init}\subseteq K$. Holds since $\it{Init}$ is included in every invariant.
  • $sp(K,r)\subseteq K$

Let $x$ be an arbitrary member of $sp(K,r)$.

\begin{equation*}
\begin{align}
x\in sp(K,r) &\Longleftrightarrow \exists y. y\in K\wedge(y,x)\in r \\
&\Longleftrightarrow \exists y.(\exists I\in \textit{Invs}1.y\in I)\wedge(y,x)\in r\\
&\Longleftrightarrow \exists I\in\textit{Invs}1.\exists y.y\in I\wedge(y,x)\in r\\
&\Longleftrightarrow \exists I\in\textit{Invs}1.x\in sp(I,r)\\
\mbox{Since $I$ is an invariant,}\\
&\Longrightarrow \exists I\in\textit{Invs}1.x\in I\\
&\Longleftrightarrow x\in K\\
\end{align}
\end{equation*}

  • $K\subseteq \textit{Good}$. Holds if $\textit{Invs}$ is non-empty.

If $\textit{Invs} \neq\emptyset$ and $\textit{Invs}1 = \textit{Invs}$ we claim $K = wp(r^*,\textit{Good})$.

To prove that $K = wp(r^*,\textit{Good})$ is the top element we have to prove the following.

\begin{equation*}
 \forall I\in\it{Invs}. I\subseteq wp(r^*,\textit{Good})
\end{equation*}

We prove the following lemme using induction on $n$.

\begin{equation*}
 \forall I\in\textit{Invs}.\forall n\in\mathbb{N}. I\subseteq wp(\bigcup_{i = 0}^{n} r^i,\textit{Good})
\end{equation*}

Base. Assume $n = 0$.

We show $\forall I\in\textit{Invs}. I\subseteq wp(r^0,\it{Good})$.

\begin{equation*}
\begin{align}
\forall I\in\textit{Invs}.I\subseteq wp(r^0,\it{Good}) &\Longleftrightarrow \forall I\in\textit{Invs}.I\subseteq wp(\Delta_S,\it{Good})\\
&\Longleftrightarrow \forall I\in\textit{Invs}. I\subseteq\it{Good}
\end{align}
\end{equation*}

This holds according to the definition of invariants.

Inductive step. Assume $\forall I\in\textit{Invs}. I\subseteq wp(\bigcup_{i = 0}^{n} r^i,\textit{Good})$. We show $\forall I\in\textit{Invs}. I\subseteq wp(\bigcup_{i = 0}^{n+1} r^i,\textit{Good})$.

\begin{equation*}
\begin{align}
\forall I\in\textit{Invs}. I\subseteq wp(\bigcup_{i = 0}^{n+1} r^i,\textit{Good})
&\Longleftrightarrow \forall I\in\textit{Invs}. I\subseteq wp(\bigcup_{i = 0}^{n} r^i\cup r^{n+1},\textit{Good})\\
&\Longleftrightarrow \forall I\in\textit{Invs}. I\subseteq (wp(\bigcup_{i = 0}^{n} r^i,\textit{Good})\cap wp(r^{n+1},\it{Good})) \\
&\Longleftrightarrow (\forall I\in\textit{Invs}.I\subseteq wp(\bigcup_{i = 0}^{n} r^i,\textit{Good}))\wedge (\forall I\in\textit{Invs}.I\subseteq wp(r^{n+1},\it{Good})) \\
\mbox{By the induction assumption,}\\
&\Longrightarrow \forall I\in\textit{Invs}.I\subseteq wp(r^{n+1},\it{Good})\\
&\Longleftrightarrow \forall I\in\textit{Invs}.I\subseteq wp(r^{n}\circ r,\it{Good})\\
&\Longleftrightarrow \forall I\in\textit{Invs}.I\subseteq wp(r,wp(r^{n},\it{Good}))\\
\end{align}
\end{equation*}

By the induction assumption we know $\forall I\in\textit{Invs}. I\subseteq wp(\bigcup_{i = 0}^{n} r^i,\textit{Good})$.

We can also easily show for two invariants $I$ and $I_1$ that $I\in \textit{Invs}\wedge I\subseteq I_1\Longrightarrow I\subseteq wp(r,I_1)$. Note that the condition $sp(I,r)\subseteq I$ is equivalent to $I\subseteq wp(r,I)$.

This proves the lemma.

Solution g)

The ordered set $\langle \textit{Invs},\subseteq\rangle$ is a lattice. We proved in part (c ) and (d) that for any $I_1,I_2\in\textit{Invs}$ both $I_1\sqcap I_2$ and $I_1\sqcup I_2$ exist and are equal to $I_1\cap I_2$ and $I_1\cup I_2$ respectively.

We showed in part (e) and (f) that for every subset $\textit{Invs}1$ both lub and gub exist: $\sqcap \textit{Invs}1=J$ and $\sqcup \textit{Invs}1=K$.

The lattice is complete. The top element is $wp(r^*,\textit{Good})$ and the bottom element is $sp(\textit{Init},r^*)$.

 
sav10/invariants_exercises.txt · Last modified: 2015/04/21 17:34 (external edit)
 
© EPFL 2018 - Legal notice