JML中的Java排序方法

我需要JML的排序方法我嘗試過Insertion Sort，但我不知道需要什麼，並確保或維護我需要的東西。請幫忙。我需要// @需要，// @確保和// @維護。JML中的Java排序方法

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; 
    } 
} 
}

來源

2017-12-27 Razvan

以下內容確保升序並保留重複。

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

來源

2018-01-20 04:56:37

JML中的Java排序方法

回答

相關問題