## OpenJML Examples: Heap Sort

Given an array of integers, sort it in-place in descending order. This implementation uses the O(n log n) heap sort algorithm. However, it does not prove the output is a permutation of the input.

Contributed by Viktorio S. el Hakim.

``````// This example was written by Viktorio S. el Hakim - 1/2021
// It establishes that the array is sorted, but not that it is a permutation of the input array

public class HeapSort {

/*@ requires 1 <= i <= len/2 && len <= arr.length;
requires \forall int k;i < k <= len/2;arr[k-1] <= arr[2*k-1];
requires \forall int k;i < k <= (len-1)/2;arr[k-1] <= arr[2*k];
ensures \forall int k;i <= k <= len/2;arr[k-1] <= arr[2*k-1];
ensures \forall int k;i <= k <= (len-1)/2;arr[k-1] <= arr[2*k];
@*/
public static void heapify(/*@ non_null @*/ int [] arr, final int i, final int len) {
int j = i;
/*@ loop_invariant i <= j <= len;
loop_invariant \forall int k; j < k <= len/2; arr[k-1] <= arr[2*k-1];
loop_invariant \forall int k; j < k <= (len-1)/2; arr[k-1] <= arr[2*k];
loop_invariant \forall int k; i <= k < j && k <= len/2; arr[k-1] <= arr[2*k-1];
loop_invariant \forall int k; i <= k < j && k <= (len-1)/2; arr[k-1] <= arr[2*k];
loop_invariant \forall int k; 2*j-1 <= k-1 <= 2*j && k <= len && j > i;
arr[k-1] >= arr[j/2-1];
decreasing len-j;
@*/
while (true) {
int m = j;
if (m <= len/2) {
int c = 2*m;
if (arr[c-1] < arr[m-1]) m=c;
if (c < len && arr[c] < arr[m-1]) m=c+1;
}

if (m==j) break;
int tmp = arr[j-1];
arr[j-1] = arr[m-1];
arr[m-1] = tmp;
j = m;
}
}

/*@
requires 1 <= len <= arr.length;
requires \forall int k; 1 <= k <= len/2; arr[k-1] <= arr[2*k-1];
requires \forall int k; 1 <= k <= (len-1)/2; arr[k-1] <= arr[2*k];
ensures  \result && \forall int k; 0 < k < len; arr[k] >= arr[0]; //Always true
public static pure model boolean isGeq(final  non_null  int [] arr, final int len) {
loop_invariant 0 <= i < len;
loop_invariant \forall int k;i < k < len;arr[k] >= arr[0];
decreasing i;
for (int i = len-1; i > 0; i--) {
int j=i+1;

loop_invariant 1 <= j <= i+1;
loop_invariant arr[i] >= arr[j-1];
decreasing j;
while(j > 1) {
j = j / 2;
}
}
return \forall int k; 0 < k < len; arr[k] >= arr[0];
}
@*/

/*@
ensures \forall int k,j; 0 <= k < j < arr.length; arr[k] >= arr[j];
@*/
public static void sort(/*@ non_null @*/ int [] arr) {
// Array of size 1 is already sorted
if (arr.length < 2) return;

// Build heap
/*@ loop_invariant 0 <= i <= arr.length/2;
loop_invariant \forall int k; i < k <= arr.length/2; arr[k-1] <= arr[2*k-1];
loop_invariant \forall int k; i < k <= (arr.length-1)/2; arr[k-1] <= arr[2*k];
decreasing i;
@*/
for (int i = arr.length/2; i > 0; i--) {
heapify(arr,i,arr.length);
}

// Now sort
int tmp;
/*@ loop_invariant 1 <= len < arr.length;
loop_invariant \forall int k;1 <= k <= (len+1)/2; arr[k-1] <= arr[2*k-1];
loop_invariant \forall int k;1 <= k <= len/2; arr[k-1] <= arr[2*k];
loop_invariant isGeq(arr,len+1);
loop_invariant \forall int k,j; 0 <= k <= len < j < arr.length; arr[j] <= arr[k];
loop_invariant \forall int k,j; len <= k < j < arr.length; arr[j] <= arr[k];
decreasing len-1;
@*/
for (int len = arr.length-1; len>1; len--) {
tmp = arr[0];
arr[0] = arr[len];
arr[len] = tmp;
heapify(arr,1,len);
}
tmp = arr[0];
arr[0] = arr[1];
arr[1] = tmp;
}
}

``````