Contract使ってみた

プログラミング C#

以下、ネガティブな記事です。

public void compute(List<List<double>> A, List<double> b) {
  Contract.Requires(A != null);
  Contract.Requires(b != null);
  Contract.Requires(A.Count >= 3);
  Contract.Requires(A[0] != null);
  Contract.Requires(A[0].Count == A.Count);
  Contract.Requires(A.Count == b.Count);
  Contract.Requires((new Func<bool>(() =>
      Enumerable.Range(0, A.Count).SelectMany(
          i => Enumerable.Range(0, A[0].Count),
          (i, j) => Math.Abs(i - j) <= 1
              ? true
              : A[i][j] < 1e-10 /* A[i][j] == 0 */
          ).All(x => x)
      ))());

compute(
    new List<List<double>> {
        new List<double> { 1, 2, 0 },
        new List<double> { 1, 2, 3 },
        new List<double> { 0, 2, 3 },
        new List<double> { 4, 2, 3 } },
    new List<double> { 4, 5, 6, 7 });


上のコードをビルドすると、チェックが走って以下のログが出力ウィンドウに表示される。
unprovenというのはチェックできないという意味らしい。
localtionの行をダブルクリックすると違反している契約にジャンプできる。

<path>\src\Main\Program.cs(17,17): warning : CodeContracts: requires unproven: A[0] != null
<path>\src\TridiagonalSolver\GaussianElimination.cs(21,13): warning :   + location related to previous warning
<path>\src\Main\Program.cs(27,17): warning : CodeContracts: Possibly calling a method on a null reference 'v'
<path>\src\Main\Program.cs(17,17): warning : CodeContracts: requires unproven: A[0].Count == A.Count
<path>\src\TridiagonalSolver\GaussianElimination.cs(22,13): warning :   + location related to previous warning
CodeContracts: Main: OutputError,requires unproven: (new Func<bool>(() =>
CodeContracts: Main: \n                Enumerable.Range(0\, A.Count).SelectMany(
CodeContracts: Main: \n                    i => Enumerable.Range(0\, A[0].Count)\,
CodeContracts: Main: \n                    (i\, j) => Math.Abs(i - j) <= 1
CodeContracts: Main: \n                        ? true
CodeContracts: Main: \n                        : A[i][j] < 1e-10 /* A[i][j] == 0 */
CodeContracts: Main: \n                    ).All(x => x)
CodeContracts: Main: \n                ))(),,,top,True,False,warning,<path>\src\\Main\\Program.cs,17,17,23,81
<path>\src\TridiagonalSolver\GaussianElimination.cs(24,13): warning :   + location related to previous warning

Contractでチェックできるのは引数などの呼び出し側からアクセス可能な変数。
privateなメンバ変数をチェックすることはできない。（忘れたけどwarning表示だったかな。）
あとはPureAttributeになっているものをContract内に書けるらしい。


A[0]やA[0].Countがunprovenになっている。
インデクサがPureになっていないという理由か？
検証できないと言っているっぽい。
とはいえ、Listのインデクサは触れないコードだ。


途中で出ている長ったらしい出力は二次元のListが三重対角行列であるかをチェックしているコードなのだが、
この中で使っているメソッドも全滅っぽい。
# 表示がなんか変ですね。


.NET Frameworkのライブラリが完全にサポートされていない状況を見るに、Contractでなんでもチェックしようと考えてはダメみたいですね。
Contractを埋め込もうとしているアセンブリが、対応していないアセンブリに依存していると、
unprovenになる状況が生まれやすくなると思います。
引数のnullチェック程度の比較的簡単なものに留めるのがいいのかもしれないと思いました。


使いどころが難しそうです。


VS2015Communityで確認しました。
Contractを使うためにはCode Contracts for .NETが必要です。