\section{Proofs of Theorems \label{proofs}}
In this section, we present the proofs of the theorems described in the paper. We first describe the Hoare triple notation that we use in the proofs.
\vspace*{1mm}
\noindent {\bf Hoare triple}. \ If $Q$ and $R$ are state predicates and $ac$ is an adaptation (sequence of atomic adaptations), then the Hoare triple is denoted as $\{Q\}ac\{R\}$ and it means that if adaptation $ac$ is begun in a state satisfying $Q$, then it is guaranteed to terminate in a finite amount of time in a state satisfying $R$. $Q$ and $R$ are referred to as the precondition and postcondition for the triplet, respectively.
\vspace*{1mm}
\noindent {\bf Theorem 1}. \ {\em Given $S_P$ as the invariant of the program before adaptation and $S_Q$ as the invariant of the program after adaptation, if there is a transitional-invariant lattice for an adaptation with entry node associated with $S_P$ and exit node associated with $S_Q$, 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)}.
Proof. \ We prove the following hypothesis, which clearly implies that if the adaptation starts in a state where the application satisfies $S_P$ then the adaptation completes in a state where the application satisfies $S_Q$, i.e., \\$\{S_P\}\{\text{adaptation}\}\{S_Q\}$ is true.
\noindent {\em Induction Hypothesis}. If $R$ is a node in the lattice with transitional-invariant $\mathit{TS}_R$, then there exists a sequence of atomic adaptations that will lead to a state from where $S_Q$ will be satisfied, i.e., $\{\mathit{TS}_R\}\{\text{sequence of atomic adaptations}\}\{S_Q\}$.
The proof is by induction on the length of the longest path from node $R$ to the exit node. Since the lattice has only one exit node, either $R$ is the exit node or there is a path from $R$ to the exit node. If the longest path has length $0$, the hypothesis clearly holds, since $R$ is the exit node and $\mathit{TS}_R = S_Q$.
Now, assume that the hypothesis holds for nodes whose longest path to the exit node has length $n \geq 0$, and consider a node $R$ whose longest path to the exit node has length $n+1$. Let the nodes reached by outgoing edges from $R$ be labeled $R_1, R_2, ..., R_k$ with corresponding edges labeled $a_1, a_2, ..., a_k$. By definition of transitional-invariant lattice, at some time one $a_i$ will be performed and $\{\mathit{TS}_{R}\} a_i \{\mathit{TS}_{R_i}\}$ is true. This implies that $\{\mathit{TS}_R\}a_i\{\mathit{TS}_{R_1} \vee \mathit{TS}_{R_2} \vee ... \vee \mathit{TS}_{R_k}\}$ is true. By the induction hypothesis, $\{\mathit{TS}_{R_i}\}\{\text{sequence of atomic adaptations}\}\{S_Q\}$ for $i = 1, 2, ..., k$ is true.
Therefore, $\{\mathit{TS}_{R_1} \vee \mathit{TS}_{R_2} \vee ... \vee \mathit{TS}_{R_k}\}\{\text{sequence of atomic adaptations}\}\{S_Q\}$ is true. It follows that $\{\mathit{TS}_R\}\{\text{sequence of atomic adaptations}\}\{S_Q\}$ is true.
Further, application before adaptation satisfies old specification from $S_P$ and all intermediate programs satisfies specification during adaptation from $\mathit{TS}_{R_i}$. Also, $\{S_P\}\{\text{sequence of atomic}$ $\text{adaptations}\}\{S_Q\}$ is true, i.e., the adaptation starting in a state where application satisfies $S_P$ will complete in a state where the application satisfies $S_Q$. In other words, the application satisfies the new specification when the adaptation completes. Thus, the adaptation is correct. \qed
%\pagebreak
\vspace*{1mm}
\noindent {\bf Theorem 2}. \ {\em The adaptation lattice of Fig. \ref{addfec3_til} is a transitional-invariant lattice for the adaptation of adding the proactive component (shown in Fig. \ref{sfec_progadd} and Fig. \ref{rfec_progadd}). Hence, the adaptation is correct}.
Proof. Before the adaptation starts only actions that are enabled are \texttt{send} of $s$ and \texttt{receive} of $r1$ and $r2$ and specification of the communication program is satisfied. In other words, invariant $S1 \wedge S2$ is satisfied. Hence, the entry node is labeled with $S1 \wedge S2$.
The program actions add a message into $\text{rQ1}$ (and, $\text{rQ2}$) only if that message is received from $s$. Thus, $S1 = \forall i : (m_i \in \text{rQ1} \vee m_i \in \text{rQ2}) \Rightarrow m_i \in \text{mQ}$ is always true.
The adaptation starts when atomic adaptation $\text{s\_block}$ is performed. At this point, none of the actions of $s$ are enabled and only \texttt{receive} actions of $r1$ and $r2$ are enabled. Thus, no new messages are added to the channels and no messages are removed from $\text{sQ}$. Clearly, ($S1 \wedge S2$) continues to hold, which is shown by $\mathit{TS}_1$ in the lattice.
Due to execution of \texttt{receive} actions of $r1$ and $r2$, eventually $\#ch.s.r1 = 0$ and $\#ch.s.r2 = 0$ respectively. The guard $\#ch.s.r1=0$ enables atomic adaptation $\text{r1\_replace}$ and $\#ch.s.r2=0$ enables atomic adaptation $\text{r2\_replace}$. After both these atomic adaptations are performed, none of the actions of $s$ are enabled, and since the channels are empty the actions of $r1$ and $r2$ are also not enabled. Thus, the message is either not sent and is in $\text{sQ}$ or it is received by the receivers and is in $\text{rQ1}$ and $\text{rQ2}$. The transitional-invariant $\mathit{TS}_4$ holds.
Atomic adaptation $\text{e\_add}$ adds the FEC encoder fraction at $s$. At this point, the actions of the encoder fraction are enabled at $s$. The \texttt{encode} action encodes the group of $(n-k)$ packets and stores it in $\text{encQ}$. The packets from $\text{encQ}$ are sent to $r1$ and $r2$. The decoder at $r1$ (respectively, $r2$) receives the packets from the channel and stores it in $\text{rbufQ1}$ (respectively, $\text{rbufQ2}$). When at least $(n-k)$ packets from a group are received, the \texttt{decode} action decodes the packets and stores the messages (data packets) in $\text{rQ1}$ (respectively, $\text{rQ2}$). Thus, a message is either in $\text{sQ}$ or it is in its encoded form in $\text{encQ}$ or in $\text{ch.s.r1}$ (respectively, $\text{ch.s.r2}$) or in $\text{rbufQ1}$ (respectively, $\text{rbufQ2}$) or the message is in $\text{rQ1}$ (respectively, $\text{rQ2}$). Clearly, the invariant $S_Q = $($S1 \wedge SF$) of the application using proactive component is satisfied. Thus, the adaptation of adding the proactive component is correct. \qed
\vspace*{1mm}
\noindent {\bf Theorem 3}. \ {\em Let $S_P$ be an invariant of the program before adaptation and let $T_P$ be the faultspan used to show that the program before adaptation is tolerant to $F_P$. Likewise, let $S_Q$ be an invariant of the program after adaptation and let $T_Q$ be the faultspan used to show that the program after adaptation is tolerant to $F_Q$. If there exists a transitional-faultspan lattice with entry node associated with $S_P$ and $T_P$, and exit node associated with $S_Q$ and $T_Q$, then the adaptation depicted by that lattice is correct in presence of $F = F_P \cap F_Q$ (i.e., while the adaptation is being performed the specification and fault-tolerance requirements during adaptation are satisfied and after the adaptation completes, the application satisfies the new specification and fault-tolerance requirements)}.
Proof. \ Since the application before adaptation is $F_P$-tolerant, and $F \subset F_P$, the application before adaptation is also $F$-tolerant. Similarly, since the application after adaptation is $F_Q$-tolerant, and $F \subset F_Q$, the application after adaptation is also $F$-tolerant. Therefore, let $T$ be the $F$-span of the application before adaptation and $T^{\prime}$ be the $F$-span of the application after adaptation. We prove the following hypothesis, which clearly implies $\{T\}\{\text{adaptation}\}\{T^{\prime}\}$.
\noindent {\em Induction Hypothesis}. If $R$ is a node in the lattice with transitional-faultspan $TT_R$, then there exists a sequence of adaptive actions that will lead to a state from where $T^{\prime}$ will be satisfied, i.e., $\{TT_R\}\{\text{sequence of atomic adaptations}\}\{T^{\prime}\}$ is true.
The proof is by induction on the length of the longest path from node $R$ to the exit node. Since the lattice has only one exit node, either $R$ is the exit node or there is a path from $R$ to the exit node. If the longest path has length 0, the hypothesis clearly holds, since $R$ is the exit node and $\mathit{TT}_R = T^{\prime}$.
Now, assume that the hypothesis holds for nodes whose longest path to the exit node has length $n \geq 0$, and consider a node $R$ whose longest path to the exit node has length $n+1$. Let the nodes reached by outgoing edges from $R$ be labeled $R_1, R_2, ..., R_k$ with corresponding edges labeled $a_1, a_2, ..., a_k$. By definition of transitional-faultspan lattice, at some time one $a_i$ will be performed and
$\{\mathit{TS}_R\} a_i \{\mathit{TS}_{R_i}\}$, or $\{\mathit{TT}_R\} a_i \{\mathit{TT}_{R_i}\}$ is true. Since, $\mathit{TS}_R \Rightarrow \mathit{TT}_R$ and $\mathit{TS}_{R_i} \Rightarrow \mathit{TT}_{R_i}$, it implies that $\{\mathit{TT}_R\} a_i \{\mathit{TT}_{R_i}\}$ is true. Thus, \\$\{\mathit{TT}_R\}\{\text{sequence of atomic adaptations}\}\{\mathit{TT}_{R_1} \vee \mathit{TT}_{R_2} \vee ... \vee \mathit{TT}_{R_k}\}$ is true. \\By induction hypothesis, $\{\mathit{TT}_{R_i}\}\{\text{sequence of atomic adaptations}\}\{T^{\prime}\}$ for $i = 1, 2, ..., k$ is true.
Therefore, $\{\mathit{TT}_{R_1} \vee \mathit{TT}_{R_2} \vee ... \vee \mathit{TT}_{R_k}\}\{\text{sequence of atomic adaptations}\}\{T^{\prime}\}$ is true. It, thus, follows that $\{\mathit{TT}_R\}\{\text{sequence of atomic adaptations}\}\{T^{\prime}\}$ is true.
Further, application before adaptation satisfies safety from $S_P$ and $T$ is the $F$-span of the application before adaptation. All intermediate $\mathit{TS}_{R_i}$ satisfies safety during adaptation from $\mathit{TT}_{R_i}$. Also, $\{T\}\{\text{sequence of atomic adaptations}\}\{T^{\prime}\}$, i.e., the adaptation starting in a state where application satisfies $T$ will complete in a state where $T^{\prime}$ is satisfied. Since $F \subset F_Q$, when the adaptation completes, the new application is in $F_Q$-span. Thus, the new application continues to be $F_Q$-tolerant from $S_Q$ after adaptation. Therefore, the adaptation is correct and meets fault-tolerance requirements. \qed
\vspace*{1mm}
\noindent {\bf Theorem 4}. \ {\em The adaptation lattice of Fig. \ref{fec2ack_til} is a transitional-faultspan lattice for the adaptation of replacing the proactive component with the reactive component (shown in Fig. \ref{sfec_ack} and Fig. \ref{rfec_ack}). Hence, the adaptation is correct in the absence of faults and in the presence of faults $F1 \cap F2$ (cf. Fig. \ref{f1} and Fig. \ref{f2})}.
Proof. \ Before adaptation starts, the application satisfies its invariant $S_P$ and fault-span $T_P$. The adaptation starts when atomic adaptation $\text{e\_block}$ is performed. Now, the FEC encoder fraction is blocked from encoding more packets. The packets that are already encoded are sent to the receivers. The application continues to satisfy $S_P = T_P$. Additionally, $\forall j:j \geq u:: \text{Empty}(\text{encQ}[j, 0..n-1]) \wedge (l \leq u)$ is also satisfied, which is shown by $\mathit{TS}_1$ and $\mathit{TT}_1$ in the lattice. Once all the encoded packets are sent, the encoder is removed. This is shown by atomic adaptation $\text{e\_remove}$. At this point the application satisfies $\mathit{TS}_2$. The faults $F$ preserves $\mathit{TS}_2$, which is shown by $\mathit{TT}_2 = \mathit{TS}_2$.
Due to execution of receive actions of $r1$ and $r2$, eventually $\#ch.s.r1=0$ and $\#ch.s.r2=0$ respectively. The guard $\#ch.s.r1=0$ enables atomic adaptation $d1\_replace$ and $\#ch.s.r2=0$ enables atomic adaptation $\#d2\_replace$. After both these atomic adaptations are performed, none of the actions of $s$ are enabled, and since the channels are empty the actions of $r1$ and $r2$ are also not enabled. The transitional-invariant $\mathit{TS}_5$ is satisfied, and since faults preserve $\mathit{TS}_5$, we have $\mathit{TT}_5 = \mathit{TS}_5$.
Atomic adaptation $\text{e\_add}$ adds the ACK send fraction at $s$. At this point, the actions of the ACK send fraction are enabled at $s$, which copies the message from $\text{sQ}$ into two queues $\text{sQ1}$ and $\text{sQ2}$. The messages from $\text{sQ1}$ and $\text{sQ2}$ are sent to receivers $r1$ and $r2$, respectively. The application satisfies $S_Q = S_1 \wedge \mathit{SA}$ if no faults $F$ occur and satisfies $T_Q = S_1 \wedge \mathit{TA}$ if faults $F$ occur.
Thus, the adaptation of replacing the proactive component with reactive component is correct and meets fault-tolerance requirements. \qed