契約アノテーション

仕組み

どのようにして契約上のアノテーションを使用することができるのかを簡単に理解するには、以下の例を参照してください。

この例では、 Adjust 関数を contract アノテーション属性で修飾しました。 この場合の属性引数は、null 引数が常に NULL を返すことを意味します。 この例のコードを読んで、このように機能することを簡単に確認できますが、現実のコードでは、この依存関係はそれほど明白ではないかもしれません。 ここでの主なものは、関数が入力値をどのように扱うかを記述する契約アノテーション属性です。

Adjust 関数を 'null' 引数で呼び出すと、JetBrains Rider は一度に多くの問題を 見つけてハイライトします。 まず第一に、この式が常に null であることを警告しながら、null 引数を持つ関数呼び出しをハイライトします。 それから、この式で初期化された adjusted 変数を追跡し続け、現在は 'null' でもあります。 adjusted 変数が 'null' と等しくないか確認すると、JetBrains Rider はこの比較は常に false であると再度警告します。 最後に、JetBrains Rider は 'if' ステートメント内のコードを到達不能としてグレー表示します：

契約アノテーションの構文

契約アノテーションの入出力関係の依存関係を指定するには、次の構文を使用します。

input は次のいずれかです。

• 参照型パラメーターの null/notnull

• ブールパラメーターの true/false

output を指定できます

• 参照型の戻り値の null/notnull/canbenull

• ブール型の戻り値の true/false

• halt | stop | void | nothing （交換可能）は、関数が正常に戻らないことを示します。 つまり、例外をスローするか、プログラムの実行を停止します。

オプションのブール forceFullStates パラメーター（デフォルトでは false）を使用すると、nullability 分析の 悲観的モードを強制できます。 つまり、メソッドの戻り値が契約条件で定義されていない場合、JetBrains Rider はそれが null である可能性があると想定します。

備考：

• パラメーターが 1 つの場合は、 paramName を省略できます（上記の例を参照）

• パラメーターがない場合は、 paramName と input の両方を省略できます：

  [ContractAnnotation("=> halt")] public void TerminationMethod()

  または、関数が入力に関係なく同じ出力となる場合：

  [ContractAnnotation("=> halt")] public void TerminationMethod(object data, bool flag)

• 同じパラメーターに対して複数の条件を追加できます。

  [ContractAnnotation("input:null => null; input:notnull=>notnull")] public object Transform(object input, bool flag)

• 条件を反転させることもできます。つまり、 input => output は output <= input と等しいことになります：

  [ContractAnnotation("null <= surname:null")] public string GetName(string surname)

• 'out' パラメーターの期待値を指定することもできます。 同じ入力条件に対して戻り値と出力パラメーターの両方を指定する場合は、コンマを使用します。

  [ContractAnnotation("s:null => false,result:null")] public bool TryParse(string s, out object result)

契約条件の検証

ソースコードで契約アノテーションを関数に付与すると、JetBrains Rider は関数シグネチャーに従って契約条件を検証します。 契約アノテーションが関数パラメーターに合わない場合、JetBrains Rider は警告を表示します：

契約アノテーションが戻り値に合わない場合も同じことが起こります。