コード コントラクトを含む次のコードでいくつかの警告が表示されます。
public static int Min(IEnumerable<int> set)
{
Contract.Requires(set != null);
Contract.Requires(set.Any());
Contract.Ensures(Contract.ForAll(set, x => x >= Contract.Result<int>()));
int min = set.Min();
return min;
}
static void Main(string[] args)
{
Console.WriteLine(Min(new int[] {3,4,5}));
Console.WriteLine(Min(new int[] {})); // should fail
}
次の警告が表示されます。
Requires unproven: set.Any() on Min(new int[] {3,4,5})
Ensures unproven: Contract.ForAll(set, x => x > Contract.Result<int>())
2 つの質問:
私の事後条件には x >= Contract.Result() と記載されていますが、「証明されていないことを保証する」という警告には x > Contract.Result() と記載されています。(Greater or equal vs. Greater) これはどうして起こるのでしょうか?
上記のステートメントで set.Any() を証明できないのはなぜですか?
前もって感謝します。