JML의 자바 정렬 방법

Question

JML에 대한 정렬 방법이 필요합니다. 삽입 정렬을 시도했지만 필요한 항목과 필요한 항목 또는 maintaingins을 모르겠습니다. 도와주세요. // @ requires, // @ ensure 및 // @ maintain이 필요합니다.

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[])