\section{Verifying Adaptation in Absence of Faults \label{til-sec}}
In this section, we introduce the notion of {\em transitional-invariant lattice} to verify the correctness of adaptation. The idea of transitional-invariant lattice is based on the concept of {\em proof lattice} \cite{provingliveness-owicki}, which is used to prove liveness properties of a concurrent program.
\noindent As discussed in Section \ref{model}, the program during adaptation consists of actions of the old program and actions of the new program. Therefore, we consider intermediate programs obtained after one or more atomic adaptations. Similar to the invariants that are used to identify ``legal'' program states and are closed under program execution, we define {\em transitional-invariants}.
\noindent {\bf Transitional-invariant}. \ Let $R$ be an intermediate program in the adaptation $\Delta$. A {\em transitional-invariant} is a predicate that is closed in $R$.
Note that the actions of intermediate program are the old program actions that are not yet removed and the new program actions that are already added. However, the adaptive actions do not necessarily preserve the transitional-invariant. Now, we define {\em transitional-invariant lattice}.
\noindent {\bf Transitional-invariant lattice}. \ A {\em transitional-invariant lattice} is an adaptation lattice with each node having one predicate and that satisfies the following five conditions:
\begin{enumerate}
\item[1.] {\bf Safety of old program}. \ The start node $P$ is associated with an invariant $S_P$ of the program before adaptation.
\item[2.] {\bf Safety of new program}. \ The end node $Q$ is associated with an invariant $S_Q$ of the program after adaptation.
\item[3.] {\bf Safety of intermediate program}. \ Each intermediate node $R$ is associated with a predicate $\mathit{TS}_R$ that is a transitional-invariant for any intermediate program at $R$ (i.e., intermediate program obtained by performing adaptations from the entry node to $R$). Furthermore, any intermediate program at $R$ satisfies the (safety) specification during adaptation from $\mathit{TS}_R$.
\item[4.] {\bf Safety of adaptive action}. \ If a node labeled $R_i$ has an outgoing edge labeled $a$ to a node labeled $R_j$, then for all adaptive transitions $(s, a, s^\prime)$ in $S_{\textit{map}}$ where $\mathit{TS}_{R_i}$ is true in state $s$, $\mathit{TS}_{R_j}$ is true in state $s^\prime$. Furthermore, all the adaptive transitions $(s, a, s^\prime)$ satisfies the safety specification during adaptation.
\item[5.] {\bf Progress of adaptation}. \ If a node labeled $R$ has outgoing edges labeled $a_1, a_2, ..., a_k$ to nodes labeled $R_1, R_2, ..., R_k$, respectively, then in all computations of adaptation there exists a transition $(s, s^\prime)$ such that for some $i : 1 \leq i \leq k : (s, a_i, s^\prime) \in S_{\textit{map}}$. Furthermore, $\forall s: s \in \mathit{TS}_R : (\forall a, s^\prime: a \in \Sigma_a - \{a_1, ..., a_k\} : (s, a, s^\prime) \not\in S_{\textit{map}})$.
\end{enumerate}
%{\em Remark}. \ An intermediate node $R$ could be reached by multiple paths. Therefore, it is required that $\mathit{TS}_R$ be met for each intermediate program corresponding to the path. Typically, when a node $R$ is reached through multiple paths, the intermediate programs obtained through those paths are same/similar.
\noindent {\bf Correctness of Adaptation}. \ Intuitively, an adaptation is correct if the following conditions are satisfied: If the adaptation begins in a legitimate state of the old program then during adaptation safety during adaptation is met and the resulting state of the new program is legitimate. With this intuition, if adaptation begins in a state where invariant of the old program is true, then we say that adaptation is correct if:
\begin{itemize}
\item Adaptation terminates in a state where invariant of the new program is true
\item During adaptation safety specification during adaptation is satisfied
\item Eventually adaptation terminates
\end{itemize}
The following theorem states that finding a transitional-invariant lattice is necessary and sufficient for proving correctness of adaptation.
\noindent {\bf Theorem 1}. \ {\it Given $S_P$ as the invariant of the program before adaptation and $S_Q$ as the invariant of the program after adaptation, the adaptation from $P$ to $Q$ is correct if and only if there is a transitional-invariant lattice for the adaptation with start node associated with $S_P$ and end node associated with $S_Q$.}
\vspace*{0.5mm}
\noindent {\em Proof}.
\noindent ($\Rightarrow$) If transitional-invariant lattice exists then adaptation is correct.
If the stated conditions are satisfied, then the specification of old program is satisfied when the adaptation starts. Also, the existence of transitional-invariant lattice during adaptation ensures that for each intermediate program that occurs during adaptation, the specification during adaptation is satisfied. Moreover, from the definition of transitional-invariant lattice, each adaptive action satisfies safety specification during adaptation. Also, in each intermediate program eventually some adaptive action will be executed, which ensures liveness of adaptation. Furthermore, the last adaptive action terminates in the invariant of the new program, from where the system satisfies the behavior of the new program. Thus, the existence of transitional-invariant lattice proves correctness of adaptation.
\noindent ($\Leftarrow$) If adaptation is correct then transitional-invariant lattice exists (proof by construction).
Assuming the adaptation is correct, to show the existence of the lattice, we proceed as follows. First, we identify the structure of the lattice. Then, for each node, we identify the corresponding transitional-invariant.
By definition, the transitional invariant lattice has one entry node $P$ that is associated with $S_P$, the invariant of the old program and one exit node associated with $S_Q$, the invariant of the new program. For the following discussion, let the entry node be denoted as current node.
Now, consider all computations $C$ of adaptation that start from the transitional-invariant associated with the current node. For each of these computations, identify the computation prefix until first occurrence of the atomic adaptation (including the state/program reached after the atomic adaptation). This occurrence exists since correctness of adaptation implies that eventually the program would be changed to the new program. Let $C_P$ denote the set of these computation prefixes. If $a_i$ is an atomic adaptation occurring in this set of computation prefixes then add an edge from the current node to a new node, say $R_i$. The label on the edge from the current node to $R_i$ would be $a_i$.
To identify the invariant associated with $R_i$, proceed as follows: The initial value of the invariant is $\mathit{TR}_i\textit{-init}$, where $\mathit{TR}_i\textit{-init}$ denotes the set of all states in $C$ that occur after the atomic adaptation $a_i$. Now, consider all computations of the program at $R_i$ (i.e., these computations do not include the atomic adaptation) that start from $\mathit{TR}_i\textit{-init}$. The set of states reached in this set of computation identifies the transitional-invariant $\mathit{TR}_i$ at node $R_i$. Now, this process is repeated for all possible atomic adaptations in $C_P$; this will identify the new nodes and corresponding programs and transitional-invariants at those nodes.
The above process is repeated for all newly created nodes as well. If the atomic adaptation being considered is the last adaptation in the multi-step adaptation process (i.e., the resulting program would be the new program) then the successor node is $Q$.
By construction, we can see that the transitional-invariant at each node is closed and the computation of the intermediate program from that transitional-invariant will result in execution of one of the {\em permitted} atomic adaptation and the resulting state would satisfy the constraint of the lattice. Moreover, since the adaptation is correct, when the last atomic adaptation is performed, the resulting state must be in $S_Q$. Thus, the constructed lattice meets all the constraints of the transitional-invariant lattice. \qed
\iffalse
Let adaptation consists of $n$ atomic adaptations $a_1, ..., a_n$. Consider all atomic adaptations that can occur in a state of the old program. Since the adaptation is correct, each of these atomic adaptations occur in a state of old program where $S_P$ holds, and execution of these atomic adaptations satisfies safety during adaptation.
Now, consider the intermediate program $I_1$ reached after execution of $a_1$. In all computations of the old program till the execution of $a_1$, the invariant $S_P$ is satisfied since old program is correct. Since the adaptation is correct, the intermediate program $I_1$ satisfies the specification during adaptation (otherwise $a_1$ is not a possible adaptation in a state of the old program). Once $a_1$ is executed, we consider all the computations of the intermediate program $I_1$, and identify the transitional-invariant $\mathit{TS}_{I_1}$ associated with it. Similarly, we consider all computations of the intermediate program reached after the execution of some atomic adaptation other than $a_1$ in a state of the old program, and find the transitional-invariant corresponding to that intermediate program. In this way, we construct first level of intermediate program and corresponding transitional-invariant lattice starting from the old program.
Now, for each intermediate program at first level we consider all possible atomic adaptations that can occur in some state of its computations. We can then identify the transitional-invariants at the second level in the lattice by considering all the computations of the intermediate programs reached due to execution of an atomic adaptation in a state of the corresponding intermediate programs at first level.
In this way, we can continue to find transitional-invariants at various levels in the lattice. Since the adaptation is correct, the atomic adaptation in each intermediate program at level $n-1$ will result in a state of the new program where $S_Q$ holds.
Thus, correctness of adaptation proves existence of transitional-invariant lattice. \qed
\fi
%Since adaptation is correct, it starts in a state of the old program where $S_P$ holds.
%Let $a_i, ..., a_j$ be all atomic adaptations that can occur in the old program. Let $I_i, ..., I_j$ be the intermediate programs reached due to execution of atomic adaptations $a_i, ..., a_j$ respectively. Now, since adaptation is correct, there is at least one atomic adaptation $a_i$ that does not violate safety during adaptation. Among all the atomic adaptations $a_i, ..., a_j$ that does not violate safety, there is at least one atomic adaptation that leads to the intermediate program that satisfies the specification during adaptation. Such an intermediate program exists because adaptation is correct. We can explore all the reachable states of that intermediate program to find the corresponding transitional-invariant. Let $A_1$ be set of atomic adaptations and $I_1$ be set of intermediate programs such that $\forall i: a_i \in A_1$ occurs in some state of the old program and leads to some state of intermediate program $I_i \in I_1$ such that $a_i$ and $I_i$ satisfies specification during adaptation. $I_1$ denotes the set of intermediate programs at level $1$ in the lattice. In other words, we have $\{S_P\} a_i \{\mathit{TS}_{I_i}\}$.
%If $\exists i: S_Q = \mathit{TS}_{I_i}$, then we have an adaptation path from $S_P$ to $S_Q$. If $\nexists i: S_Q = \mathit{TS}_{I_i}$, then we can do reachability analysis for each intermediate program at level $1$ and each atomic adaptation that can occur at level $1$. Since adaptation is correct, it implies liveness of adaptation. Therefore, we will be able to find at least one intermediate program at level $2$ that satisfies specification during adaptation. If one of the intermediate programs at level $2$ is the new program, we have found an adaptation path from $S_P$ to $S_Q$, otherwise we keep doing the reachability analysis till we find an adaptation path from $S_P$ to $S_Q$.
%We can find all adaptation paths from $S_P$ to $S_Q$ to get a transitional-invariant lattice.
%, then the adaptation depicted by that lattice is correct (i.e., while the adaptation is being performed the specification during adaptation is satisfied and after the adaptation completes, the application satisfies the new specification).}
%{\em Proof}. \ $S_P$ is the invariant of the old program $P$. When adaptation starts, some atomic adaptation $a_i$ occurs in a state where $S_P$ holds.
%One way to calculate the transitional-invariant of the intermediate program reached after execution of $a_i$ is to characterize the set of states that are reachable under the execution of the intermediate program (till it executes next atomic adaptation). We can follow this constructive approach and identify the transitional-invariants of all the intermediate programs.
%Since the adaptation is correct, the last atomic adaptation would end in state where invariant $S_Q$ of the new program holds. \qed