C＃代碼合同：數組操作

Question

對於大學我必須學習如何處理C＃代碼合同。

我想使用它的這種方法，應在返回數組中最小的元素：

public int minarray(int[] minarray) 

這裏是我，但我不知道這是否是正確的：

public int minarray(int[] minarray) 
{ 
    //Neither the array should be empty nor null 
    Contract.Requires(minarray != null && minarray.Length != 0); 
    //Save the result... 
    int result = Contract.Result<int>(); 
    //...and check: 
    Contract.Ensures(Contract.ForAll(0, minarray.Length, i => minarray[i] >= result)); 
} 

任何人都可以告訴我，如果這是正確的，或者我只是寫完全無意義？我會很感激。

除此之外，下一個任務說：

public int[] posnegarray(int[] posneg) 

（這應該改變的所有元素的符號的方法例如從（1，-2,3）至（-1,2，-3 ）。

public int[] posnegarray(int[] posneg) 
{ 
    //Neither the array should be empty nor null 
    Contract.Requires(posneg != null && posneg.Length != 0); 
    //Save the result... 
    int resarray = Contract.Result<int[]>(); 
    //...and check: 
    Contract.Ensures(Contract.ForAll(0, posneg.Length, i => posneg[i] == (-1) * resarray[i])); 

    int[] returnarray = new int[posneg.Length]; 
    for(int j = 0; j < posneg.Length; j++) 
     returnarray[j] = posneg[j] * (-1); 
    return returnarray; 
} 

可這是正確的嗎？

Answer 1

Contract.Result應該只有Contract.Ensures方法，它並沒有真正執行內使用，但只是表示結果。您正在使用的方式它會執行t他會返回默認的方法（對於int，它將爲0），然後在您的Ensures方法中使用該默認值，這可能不是您所期望的。你應該把Result方法放在這樣的保證範圍內：

Contract.Ensures(Contract.Result<int>() >= -1);