\begin{slide}{Die richtigen Invarianten f�r Bubble-Sort}


\begin{verbatim}
static void sort (int [] a) {
  int top = a.length-1;
  for (int i=top; i>1; i--) {
    for (int p=i+1; p <= top; p++) {
      dominates (a, p);
    }
    for (int j=0; j<i; j++) {
      dominates (a, j);
      swap_if_gt (a, j, j+1);
} } }

dominates(a,p) == 
    a[0] <= a[p] && .. && a[p-1] <= a[p]
\end{verbatim}
  
\end{slide}
