即時嘗試證明在我的集合中是否存在具有特定狀態的對象。我的集合由一個名爲getStatus（）的方法組成。現在我想證明在這個集合中是否有一個具有給定狀態的對象。 @ requires (\exists int i; 0 <= i && i < sizeLimit; orders[i].getStatus().equals(Status.New));
public Order getFirstOrd
一個JML後置條件的一類方法可以包含調用另一個方法調用 例如，我有這個類： public class A
{
public int doA(x)
{ ... }
public int doB(int x, int y)
{ ... }
}
對於DOB的後置條件，我可以有：ensures doA(x) = doA(y)？
當我嘗試在http://jmlspecs.sourceforge.net/openjml-updatesite我收到以下錯誤安裝從更新站點的openJML插件： An error occurred while collecting items to be installed
session context was:(profile=epp.package.java, phase=org.ecli
我需要JML的排序方法我嘗試過Insertion Sort，但我不知道需要什麼，並確保或維護我需要的東西。請幫忙。 我需要// @需要，// @確保和// @維護。 public class InsertionSort
{
void sort(int arr[])
{
int n = arr.length;
for (int i=1; i<n; ++i)
{