// ============================================================================
// Name:        BubbleSort
// Description: Sort an array of numbers.
// References:  R. Sedgewick. Algorithms. Addison-Wesley, 1991.
//              http://en.wikipedia.org/wiki/Category:Sort_algorithms
// Parameters:  SIZE (size of array)
//              INFINITE (use variables with infinite bit width)
//              BITS (bit width for finite variables)
// ============================================================================

#ifndef SIZE
#define SIZE 4u
#endif

#ifdef INFINITE
#define TYPE int
#else
#ifndef BITS
#define BITS 4u
#endif
#define TYPE int[BITS]
#endif

#define SORTED(a) (forall(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-2u)) a[i] <= a[i+1u])

module BubbleSort(TYPE b[SIZE], &a[SIZE], nat[sizeOf(SIZE)] &i, &j, event &ready)
   implements SortSpec(a, ready) {
   sequence(nat[sizeOf(SIZE-1u)] i=0u .. (SIZE-1u))
      a[i] = b[i];

   while (i < SIZE) {
      j = i+1u;
      while (j < SIZE) {
         if (a[i] > a[j]) {
            next(a[i]) = a[j];
            next(a[j]) = a[i];
         }
         next(j) = j+1u;
         pause;
      }
      next(i) = i+1u;
      pause;
   }

   emit ready;
}

spec SortSpec(TYPE a[SIZE], event &ready) {
   termination: A F ready;
   correctness: A G (ready -> SORTED(a));
}