Considere uma classe Sorter onde está definida uma variável \tiny a[size]

    1 template<class T, int size=10>

    2 class Sorter {

    3 public:

    4    ...

    5    void insertionSort();

    6 private:

    7    int length;

    8    T a[size];

    9 };

Considere o método insertionSort() dessa classe

   11 // Pré-condição:    a[0]...a[a.length-1] é uma array de elementos

   12 //                  T não ordenada. 

   13 // Pós-condição:    A array a está ordenada por ordem decrescente.

   14 

   15 template<class T, int size>

   16 void Sorter<T,size>::insertionSort()

   17 {

   18    for (int i = 1; i < length; i++) 

   19    {

   20       T temp = a[i];

   21       int j = i - 1;

   22       while (j >= 0 && temp > a[j])

   23       {

   24          a[j+1] = a[j];

   25          j--;

   26       }

   27       a[j+1] = temp;

   28    }

   29 }

A invariante para o ciclo mais exterior (o ciclo for) é