Skip to main content

Unit 4.4 Deriving loop invariants with the FLAME notation

Exercise 4.2.

Evaluate

  • \(p( \left( \begin{array}{c} a_0 \\ \alpha_{1} \end{array} \right) , \chi ) \) in terms of \(p( a_0, \chi ) \text{,}\) \(\alpha_1 \text{,}\) and \(\chi \text{.}\)

  • \(p( \left( \begin{array}{c} \alpha_{1} \\ a_2 \end{array} \right) , \chi ) \) in terms of \(p( a_2, \chi ) \text{,}\) \(\alpha_1 \text{,}\) and \(\chi \text{.}\)

Solution

  • By our conventions, \(a_0 \) is a vector and \(\alpha_1 \) is a scalar or, equivalently, a vector of size one (\(m( \alpha_1 ) = 1 \)).

    \(p( \left( \begin{array}{c} a_0 \\ \alpha_{1} \end{array} \right) , \chi ) = p( a_0, \chi ) + p( \alpha_1, \chi ) \times \chi^{m( a_0 )} = p( a_0, \chi ) + \alpha_1 \times \chi^{m( a_0 )} \)

  • By our conventions, \(a_2 \) is a vector and \(\alpha_1 \) is a scalar or, equivalently, a vector of size one (\(m( \alpha_1 ) = 1 \)).

    \(p( \left( \begin{array}{c} p \alpha_{1} \\ a_2 \\ \end{array} \right) , \chi ) = p( \alpha_1, \chi ) + p( a_2, \chi ) \times \chi^{m( \alpha_1 )} = \alpha_1 + p( a_2, \chi ) \times \chi \)

To determine loop invariants, we observed that (using our new notational conventions)

\begin{equation} \psi = \sum_{i=0}^{k-1} \alpha_i \chi^i + \left( \sum_{i=0}^{n-1-k} \alpha_{i+k} \chi^i \right) z ~\wedge ~ z = \chi^k ~\wedge ~ 0 \leq k \leq n. \label{OldNotation}\tag{4.1} \end{equation}

then (4.1) becomes

\begin{equation} \psi = p( a_T, \chi ) + p( a_B, \chi ) \zeta ~\wedge~ \zeta = \chi^k ~ \wedge ~ k = m( a_T ), \label{PME-FLAME}\tag{4.2} \end{equation}

which very explicitly defines the function recursively. Here, we don't need to specify that \(0 \leq k \leq n \) because the sizes of \(a_T \) and \(a_B \) are inherently constrained as needed by the fact that they are appropriate subvectors of \(a \text{.}\)

From (4.2), we can now determine the same five loop invariants as in 3.4:

\begin{equation*} \begin{array}{| l | l |} \hline {\bf Invariant~1} \amp \psi = p( a_T, \chi ) \phantom{+ p( a_B, \chi ) \zeta ~\wedge~ \zeta = \chi^k ~ \wedge ~ k = m( a_T ) } \\ \hline {\bf Invariant~2} \amp \psi = \phantom{p( a_T, \chi ) +} p( a_B, \chi ) \zeta ~\wedge~ \zeta = \chi^k ~ \wedge ~ k = m( a_T ) \\ \hline {\bf Invariant~3} \amp \psi = \phantom{p( a_T, \chi ) + } p( a_B, \chi ) \zeta ~\wedge~ \zeta = \chi^k ~ \wedge ~ k = m( a_T ) \\ \hline {\bf Invariant~4} \amp \psi = p( a_T, \chi ) \phantom{ + p( a_B, \chi ) \zeta} ~\wedge~ \zeta = \chi^k ~ \wedge ~ k = m( a_T ) \\ \hline {\bf Invariant~5} \amp \psi = \phantom{p( a_T, \chi ) + }p( a_B, \chi ) \phantom{ \zeta ~\wedge~ \zeta = \chi^k ~ \wedge ~ k = m( a_T )} \\ \hline \end{array} \end{equation*}

Here, we use Greek lower case letter zeta, \(\zeta \text{,}\) where we previously used \(z \text{.}\) Invariant 3 and 4 are identical, except that in one case \(\zeta \) is implicitly used and in the other case \(\zeta \) is to be instantiated as a variable in the program.