I need a sort method for JML I tried Insertion Sort but I don't know what requires and ensures or maintaingins I need. Please help. I need //@requires, //@ensures and //@maintaining.
public class InsertionSort
{
void sort(int arr[])
{
int n = arr.length;
for (int i=1; i<n; ++i)
{
int key = arr[i];
int j = i-1;
while (j>=0 && arr[j] > key)
{
arr[j+1] = arr[j];
j = j-1;
}
arr[j+1] = key;
}
}
}
The following ensures ascending order and preserves repetitions.