Skip to main content

Unit 4.5 Deriving algorithms with the FLAME notation

Much like we filled out a worksheet before, given a loop invariant, we can do the same with this new notation [1]. If we choose Invariant 5, then it is relatively straight forward to fill in Steps 1-5:

In this worksheet, gray boxes hold assertions and the column on the left indicates the order in which it is to be filled. To get this point, we notice that

  • Step 1a: The precondition is \(T \) since many assumptions about \(a \) and \(\chi \) are implicit in the choice of a lowercase Roman letter for the vector and a lowercase Greek letter for \(\chi \text{.}\)

    Step 1b: The postcondition is \(\psi = p( a, \chi ) \text{.}\)

  • Step 2: We fill in the Invariant 5

    \begin{equation*} \psi = \pi\left(a_B, \chi \right) \end{equation*}

    in the appropriate places.

  • Step 3: The loop guard can be termined from the fact that

    \begin{equation*} \psi = \pi\left(a_B, \chi \right) ~\wedge \neg( G ) \end{equation*}

    must imply the postcondition

    \begin{equation*} \psi = \pi\left(a, \chi \right). \end{equation*}

  • Step 4: The initialization must put the variables in a state where the loop invariant is true, which is accomplished by

    \begin{equation*} \begin{array}[b]{@{}l} \psi:=0 \\ a \rightarrow \left( \begin{array}{c} a_T \\ \hline a_B \end{array} \right), \end{array} \end{equation*}

    where \(a_B \) is empty.

  • Step 5: At each step, we expose the last entry of \(a_T \text{,}\) the top part of \(a \text{,}\) compute with it, and then move it to \(a_B \text{,}\) the bottom part of \(a \text{.}\)

Next, we notice that Steps 5a and 5b are merely indexing steps in which various parts of the vector are relabeled.

  • Step 6: The contents of \(\phi \) in terms of these exposed parts, is given by the loop invariant

    \begin{equation*} \psi = \pi\left(a_B, \chi \right) \end{equation*}

    with \(a_2 \) substituted for \(a_B \text{:}\)

    \begin{equation*} \psi = \pi\left(a_B, \chi \right). \end{equation*}

  • Step 7: At the bottom of the loop, the variables must again be in a state where

    \begin{equation*} \psi = \pi\left(a_B, \chi \right). \end{equation*}

    However, by then \(a_B \) has been expanded to add \(\alpha_1 \) as its first element. Thus, before \(a_B \) is so redefined, it must be that

    \begin{equation*} \psi = p \left( \left( \begin{array}{c} \alpha_1 \\ a_2 \end{array} \right), \chi \right), \end{equation*}

    which from 4.2 we saw equals

    \begin{equation*} \psi := \alpha_1 + p( a_2, \chi ) \times \chi. \end{equation*}

This brings fills the worksheet further:

Finally, the state of variable \(\psi \) must be updatde from that in Step 6:

\begin{equation*} \psi = \pi\left(a_B, \chi \right) \end{equation*}

to that in Step 7:

\begin{equation*} \psi := \alpha_1 + p( a_2, \chi ) \times \chi. \end{equation*}

This allows us to complete the worksheet:

Finally, we can remove all the annotations, leave us with the algoriithm:

The important observation is that this notation hides the details of indexing, both in the algorithm itself and in the annotations.