java - JML中的Java排序方法

Question

我需要一种用于 JML 的排序方法我尝试过插入排序，但我不知道我需要什么，并确保或维护我需要什么。请帮忙。我需要//@requires、//@ensures 和//@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;
    }
}
}

Answer 1

以下确保升序并保留重复。

//@ assignable arr[*];
//@ requires arr != null;
//@ ensures (\forall int i; 0 <= i && i <= arr.length-1; arr[i] <= arr[i+1]) &&
//@         (\forall int i; 0 <= i && i <= arr.length;
//@            (\num_of int j; 0 <= j && j <= arr.length;
//@               arr[i] == \old(arr[j])) ==
//@            (\num_of int j; 0 <= j && j <= arr.length;
//@               arr[i] == arr[j])
//@         );
//@            
void sort(int arr[])