// ************************************************************************** // // // // eses eses // // eses eses // // eses eseses esesese eses Embedded Systems Group // // ese ese ese ese ese // // ese eseseses eseseses ese Department of Computer Science // // eses eses ese eses // // eses eseses eseseses eses University of Kaiserslautern // // eses eses // // // // ************************************************************************** // // BubbleSort first performs the following compare/swap operations on an // // array b: (0,1); (1,2); (2,3); ..., (n-2,n-1). Then, the maximal element // // is at the rightmost position b[n-1]. After this, in round i, the swap // // operations (0,1); (1,2); (2,3); ..., (n-i-1,n-i) are performed, so // // that b[n-i..n-1] contains already the final elements. The algorithm is // // called BubbleSort, since the maximal elements in the remaining part of // // the array rise up like bubbles in a fluid. // // ************************************************************************** // macro aSize = 16; macro iSize = 64; module BubbleSort([aSize]int{iSize} ?a,b, event !ready) { for(i=0..(aSize-1)) b[i] = a[i]; for(i=1..aSize-1) { for(j=1..aSize-i) { if(b[j-1] > b[j]) { next(b[j]) = b[j-1]; next(b[j-1]) = b[j]; } pause; // an invariant is here that b[j] is the max of b[0..j] assert(forall(k=0..j-1) (b[k]<=b[j])); } // an invariant is here that b[aSize-i..aSize-1] is already sorted assert(forall(k=1..i-1) (b[aSize-k-1]<=b[aSize-k])); } emit(ready); } drivenby Test01 { for(i=0..aSize-1) a[i] = i; dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); } drivenby Test02 { for(i=0..aSize-1) a[i] = aSize-1-i; dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); } drivenby Test03 { for(i=0..aSize-1) a[i] = ((i%2==0)?i:((aSize%2==0)?aSize-i:aSize-1-i)); dw: await(ready); for(i=0..aSize-1) assert(b[i] == i); }