JML中的Java排序方法

  • Z时代
  • 2024-01-10
  • 分类：问答

我需要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; 
    } 
} 
}

回答：

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

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

以上是 JML中的Java排序方法 的全部内容， 来源链接： utcz.com/qa/265818.html

回到顶部