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^*)$ .