c# - Code Contracts を使用して、空白でも null でもない val が常にメソッドから返されるようにするにはどうすればよいですか?

Question

このコード:

private static char GetBarcodeChecksumWithLegacyCode(string barcodeWithoutCzechSum)
{
    Contract.Requires(!string.IsNullOrWhiteSpace(barcodeWithoutCzechSum));
    Contract.Ensures(Contract.Result != null);
    . . .

...コンパイルされません ("演算子 '!=' は、タイプ 'メソッド グループ' および '' のオペランドには適用できません")。

これは同じように失敗します:

Contract.Ensures(Contract.ValueAtReturn != null);

コード コントラクトを使用して結果を返すメソッドの必要性を強制するにはどうすればよいですか?

アップデート

私がこれを行う場合：

Contract.Ensures(Contract.Result<char>() != '');

...「空の文字リテラル」で失敗します

これは、返された char val が null でも空でもないことをテストする方法です。

Contract.Ensures(Contract.Result<char>() != null && Contract.Result<char>().ToString() != string.Empty);

...または null チェックで十分ですか?

ところで、Result の代わりに ValueAtReturn を使用しようとすると、「メソッド 'ValueAtReturn' のオーバーロードは 0 の引数を取ります」

更新 2

このコード:

Contract.Ensures(Contract.Result<String>() != null && Contract.Result<String>() != string.Empty); 

次のエラーで失敗します:

メソッド BarcodeCzechDigitTester.Form1.GetBarcodeChecksumWithLegacyCode(System.String): 'System.String' で結果への呼び出しを検出しました。'System.Char' である必要があります。

(2 回) また: "コマンド ""C:\Program Files (x86)\Microsoft\Contracts\Bin\ccrewrite.exe" "@BarcodeCzechDigitTesterccrewrite.rsp"" はコード 2 で終了しました。 "

...しかし、コードを次のように変更すると動作します:

Contract.Ensures(Contract.Result<char>() != null && Contract.Result<char>().ToString() != string.Empty);

Answer 1

char は値型です。null にすることはできません。

char はコレクション (文字列や配列など) ではないため、空にすることはできません。

メソッドがバーコード チェックサムの数字を返す場合、コントラクトは次のようにチェックサム文字の値をチェックできます。

Contract.Ensures ( '0' <= Contract.Result<char>() && Contract.Result<char>() <= '9' );

Answer 2

次のようにする必要があります。

Contract.Ensures(Contract.Result<string>() != null);