kazuk は null に触れてしまった

C# / .NET 系技術ネタ縛りでお送りしております

タグアーカイブ: Code Contracts

VS2010 後の世代のプログラミング (2) Pex


という訳でいくつもの連載するよと言っといて(2)が来ないとかやってるとアレなので、Visual Studio 2010 リリース後に出てきた物が開発にどう影響を与えるかという事で、Pex を取り上げます。

Pex って何?

Pex は内部的には Z3 証明器の論理的証明に対するインプットをメソッドシグニチャ、および、CLRのトレース機構と結びつける事でプログラムの動作が証明された状態を近づける事をサポートします。
って説明で解るわけないっすよね。
要するにです、プログラムの断片にどんな入力を与えたらどういう分岐が発生して、どういう条件が発生してというのをトレース情報を元に補完しながら解析分析するという事をします。
Z3証明器の結果としてプログラムの動作パスが何種類か得られ、その何種類かの動作パスに飛び込むにはこのパラメータセットでその処理を呼べば良いという事が解る物を、単体テストの形式で出力してくれるのが Pex な訳です。
中がどう動くかという事はPexがトレースを元にして進行的に解析しますので、実際に何が起こるのか解らない物に対してこういうパラメータセットを与えればこういう結果を返すというのを調べてくれるのでレガシー化してしまい文書化されていない物に対して非常に強い側面もありますが、停止性問題により全てのケースを網羅できない事は数学的に証明されていて、中身をいじる事ができない物、完全なブラックボックスに対してはどっかしらで限界がありますのである程度リファクタリングが可能な物に対して適用するのが最も望ましい結果を生み出します。(Pexがお手上げになった部分をリファクタリングで切り出してあげるとさらなる進行解析が可能となってより網羅性のある解析が実行されます。)
能書きはさておき、Pexを実際に使ってみましょう。

Pexによる実行パス解析の最も単純な例

C# での checked 演算を例にとって、四則および単項演算の単純ロジックをテストするとします。
namespace PexTarget
{
    public class Class1
    {
        public int Add( int p1, int p2 )
        {
            checked
            {
                return p1 + p2;
            }
        }
    }
}
このAdd を右クリックし Pex –> Create Parameterlized Unit Test した結果の出力は以下です。
// <copyright file="Class1Test.cs" company="Microsoft">Copyright ゥ Microsoft 2011</copyright>
using System;
using Microsoft.Pex.Framework;
using Microsoft.Pex.Framework.Validation;
using Microsoft.VisualStudio.TestTools.UnitTesting;
using PexTarget;

namespace PexTarget
{
    /// <summary>This class contains parameterized unit tests for Class1</summary>
    [PexClass(typeof(Class1))]
    [PexAllowedExceptionFromTypeUnderTest(typeof(InvalidOperationException))]
    [PexAllowedExceptionFromTypeUnderTest(typeof(ArgumentException), AcceptExceptionSubtypes = true)]
    [TestClass]
    public partial class Class1Test
    {
        /// <summary>Test stub for Add(Int32, Int32)</summary>
        [PexMethod]
        public int Add(
            [PexAssumeUnderTest]Class1 target,
            int p1,
            int p2
        )
        {
            int result = target.Add(p1, p2);
            return result;
            // TODO: add assertions to method Class1Test.Add(Class1, Int32, Int32)
        }
    }
}

属性を無視してみれば単純に呼び出すコードが生成されているのが解ります。
この Class1Test の Add を右クリックして Run Pex Explorations すると
imageimage
2つの動作パスが検出されそれぞれの動作パスにおいてどういう結果となるのかが解析されました。
OverflowExceptionが望まれる結果という事でAllowException し再度 Run Last Pex Exploarations するとすべてグリーンになります。
image image image
インデントがあれとかはご愛嬌って事ですが、Class1を生成し、Addに指定パラメータを与えて実行する単体テストになっています。(TestMethod属性修飾されてますよね)
結果として以下のコードが生成されます。
namespace PexTarget
{
    public partial class Class1Test
    {
[TestMethod]
[PexGeneratedBy(typeof(Class1Test))]
public void Add602()
{
    int i;
    Class1 s0 = new Class1();
    i = this.Add(s0, 0, 0);
    Assert.AreEqual<int>(0, i);
    Assert.IsNotNull((object)s0);
}
[TestMethod]
[PexGeneratedBy(typeof(Class1Test))]
[ExpectedException(typeof(OverflowException))]
public void AddThrowsOverflowException587()
{
    int i;
    Class1 s0 = new Class1();
    i = this.Add(s0, -2147409852, -1040186368);
}
    }
}
単体テストになってますのでそのまま動かしてテストが可能です。
image
では、このテストは本当に有効なのでしょうか。テスト構成のデータ収集でコードカバレッジを有効にして
image image
リビルドしカバレッジデータを取るためにすべてのテストを再実行します。
image
はい100% ですね、これ以上有効なテストは存在しないわけです。
Pexはトレースと証明器によって少なくとも追える範囲のテストを自動的に実装しますので、単純にコードを書いてPex Explorartionした結果が望ましい物であればそれを受け入れるとするだけでカバレッジレートの非常に高いテストクラスが得られます。

Pex Driven Contract based development

という訳でPexでは Explorations の結果を見て望ましい結果が出るようにコードを直していくというサイクルでコードを実装していくことができます。
では int Sum( IEnumerable<int> sequence ) を実装してみましょう。
public int Sum( IEnumerable<int> seq )
{
    var result = 0;
    foreach (var i in seq)
    {
        result += i;
    }
    return result;
}
何も考えないで書いて、Create Parametelized Unit Test します。出来上がった Parametelized Unit Test 上で Pex Explorations すると NullReferenceException を投げるケースがあるという事が解ります。
seq が null の場合ですね。ここで Code Contracts を有効にして Contract.Require を使って seq!=null を Pre condition にすると
image image
はい、Pre condition 記述されたパラメータは自動的にPexでも認識されて無効なパラメータによる呼出しとなりました。
OverflowException が飛んでないですね。確かに checked ブロックの記述を忘れています。checkedを追加してAllow Exception すると以下になります。
imageimage
という訳で、入力で通るべきすべてのパスを網羅したテストが出来上がりました。
/// <summary>
/// 合計を計算します
/// </summary>
/// <param name="seq"> integer sequence </param>
/// <returns> sum value of sequence </returns>
/// <exception cref="ArgumentNullException"> when seq is null </exception>
/// <exception cref="OverflowException"> when overflow </exception>
public int Sum( IEnumerable<int> seq )
{
    Contract.Requires<ArgumentNullException>(seq!=null);

    var result = 0;
    foreach (var i in seq)
    {
        checked
        {
            result += i;
        }
    }
    return result;
}
Explorationsの結果を見れば exception のドキュメントコメントも容易ですね。
まぁ、これで良いのかというと、呼出し側に pre condition 規制の難しい所で例外が外に飛んで行ってしまう可能性があるわけで、設計上望ましい挙動ではないかもしれません。これを Explorations から読み取る事ができるので 「TrySum を作る」という選択肢を少なくとも検討する機会が得られるのは非常に重要な事です。
ではTrySumを作るとしましょう。
さくっと軽く書きますとこうなりますね。
public bool TrySum( IEnumerable<int> seq, out int result )
{
    Contract.Requires<ArgumentNullException>(seq != null);

    result = 0;
    foreach (var i in seq)
    {
        try
        {
            checked
            {
                result += i;
            }
        }
        catch (OverflowException)
        {
            return false;
        }
    }
    return true;
}
これを Explorations するとこうなります。
image
false 時に out パラメータに無効値が出てるのが気に入らないとか思いませんか?思う人は例外安全とか失敗時挙動の健全性なんて物に敏感という訳で。
Contract.Ensures の出番ですね。false 時には out result には0 が返ると表明します。
Contract.Ensures(
    !Contract.Result<bool>()
    ? Contract.ValueAtReturn(out result) == 0 : true );
Contractのチェックオプションを Pre condition より強くしていればこのように契約違反例外が飛びます。
image
契約違反にならない様にするために tempResult変数を導入して、tempResult 上で計算したうえで、成功時だけ値を返すようにすると以下の通り。
public bool TrySum( IEnumerable<int> seq, out int result )
{
    Contract.Requires<ArgumentNullException>(seq != null);
    Contract.Ensures(
        !Contract.Result<bool>()
        ? Contract.ValueAtReturn(out result) == 0 : true );
    result = 0;
    var tempResult = 0;
    foreach (var i in seq)
    {
        try
        {
            checked
            {
                tempResult += i;
            }
        }
        catch (OverflowException)
        {
            return false;
        }
    }
    result = tempResult;
    return true;
}
image
このように Contracts を絡めるとPexは本当に威力を発揮するわけですね。
そして出来上がったテストを本当にテストコードに含める時は Explorationsから Promote すると、本体のPex class にマージされます。
image image
当然にカバレッジレートは 100 % になりました。
このように Pex とCode Contractsを組み合わせていく事でプログラムの動作は常に把握され、表明された状態に制約されて動作する事が保障され、なおかつカバレッジレートは相当に高いテストが出来上がります。テストが出来上がるだけでなく、書いたコードがどのような動作バリエーションを起こすかをPexは素早く列挙しますのでコードを書き、それが示す挙動が自分の想定通りかを簡単に確認しながら実装を進めていくことができます。

Pexが苦手とする物

Pexにはいくつか苦手とするものがあります。多くは単体テストという方法論自体が苦手とする領域でもありますが、ここで列挙してみましょう。
  1. 値域が非常に広い物、シーケンスの後方に依存する処理
  2. MEFインポート
  3. 環境値(日付時刻、ランダム値)
Pexはトレースを元に進行解析を行いますので、値域が非常に広いものを苦手とします、また、小さなデータの組み合わせを順次拡張しながらパターンを作りテストを実行してトレース結果から新たなパスを検出するのでシーケンスの後方、たとえば 3000文字以降に何かがあれば何かするとかは生成するのに非常な繰り返し回数を必要としてしまいきっと失敗します。処理を単位に分割する等で巨大なテストケースが必要とならない様にリファクタリングをする必要があるでしょう。
Pexは非常に便利なのですが、その方法論固有の問題を内在しています。しかし実際問題としてPexがお手上げになるケースは人が単体テストを書こうとしても問題となるケースである事が多いです。であれば苦労はPex(機械)にしてもらうというのは正しい選択でしょう。これらの問題にぶつかってPexがお手上げになるケースは多くの場合リファクタリング等設計を直した方が良いケースを暗示しますのでとりあえず書いたものをPexに投げ込んでみてお手上げケースは「リファクタリングした方がいいんじゃない?」というメッセージとして素直に受け取ってみる事をお勧めします。

Pex と Code Contracts と WCF と MEF

はい、いきなりWCFです。脈絡感じないかもしれませんが WCF には Service Contract, Operation Contract, Data Contract と色々と Contract が並んでいるという訳で、これらの Contract を使ってサービスのプロトコルを記述する事ができます。このサービスのプロトコルに対して Code Contracts でインターフェース契約を記述する事ができます。実装上リモートエンドポイントに対して WCF で結合するか、MEFで実装を取り込むかは「好きにすれば?」の世界であり別に自由な話です。要するに WCF のコントラクトとしての属性記述をしなかった場合にはその自由が失われるだけで、 MEF という選択肢は残ります、MEFしない場合これまでのリポジトリパターンのように自分でサービス解決をしなさいと言われるだけです。
要するに手間数が許すなら WCF プロトコル属性でのマークアップはやっとけと、何も失うものはなく、サービスをリモートにおける自由度を獲得できるぞと。
サービスを実装したら Code Contracts と Pexで高いカバレッジを持ったテストを実装する事ができます。サービスは多くの場合サービスの利用者に対してテスト可能性を提供するモックを必要とします。では、モックを使った場合に処理が失敗したケースにおいて「モックが悪い?それともモックを呼ぶ実装が悪い?」これはややこしい問題です。モックの実装が正しく契約に従っていない等は最も駄目な話でモックの正しさは重要です。しかし、「モックをテストする?」というとこれまではやってられない話でした。しかしPexによってモックのテストの実装の大よそは実現されます。Code Contracts でのインターフェース契約が整っていれば、モックを使う側の実装が悪いといえる状況に容易に持って行けるはずです。
Code Contracts でのインターフェース契約はインターフェースの設計の重要な要素です。設計だからそれを日本語で書いて脳みそで解釈するか、コードで書いて機械が解釈するかは表現と解釈機の違いでしかない、この解釈機の厳密性と精度と速度を比較したら大よそ勝負になんてならない事は自明でしょう。
「TDDで設計をテストに!」、実行できるメリットは存在する事に異存はありません、実行できるので高い厳密性があるのも異存はありません。しかしその設計を解釈して展開するときに人間の脳みそに頼るのがTDDのテストが設計書だという時の弱さです。Code Contractsは本当に機械解釈できる設計書となり、コードを書くとき、そのコードのテストを実装するときの参照メタデータとして普遍的な表現として使われ続けます。この普遍的表現の解釈機が Code Contracts であり Pexという訳です。

ルーズスキーマと dynamic、ストロングスキーマと Contracts

LLでの動的性、ルーズスキーマを取り込むのが dynamic での C#4.0の進化点と、それだけじゃないよ、VS2010のリリースにはこぼれたけどCode ContractsとPexはストロングスキーマな静的言語の厳密性の大きな進化です。
という訳で VS2010 後の世代のプログラミング (2) でした。Code Contracts / Pex が設計に厳密性や検証性をもたらした逆方向という意味で自由度を提供する物、MEFを取り上げます。
広告

Visual Studio 2010 後の世代のプログラミング(1) Code Contracts


Visual Studio 2010 「後」って事で VS2010 には正式には組み込まれてないんだけど、その後にリリースされた各種拡張がどんな感じでプログラミングに影響を与えるかの話。

(1)って事で連載。

 

というわけで最初は Code Contracts、Code Contracts については一回書いてるけど素晴らしく使える代物って事で導入から設定まで流した上で軽くイントロダクション

まずダウンロード、DevLabs Code Contracts から Download Standard Edition / Download Premium Edition どっちか選んでインストールする。僕は Premium を選んでインストールしたぜって事でそれをベースに書きます。

(ってか Static Checker 無いと契約違反をビルド時に検出できないんで魅力半減っていうより魅力なっしんぐ)

これをインストールするとプロジェクトのプロパティに Code Contracts にページが追加されます。追加されたページを通して一通りの設定をすると、Code Contracts による契約チェックが利用できます。

まず、デバッグ設定から、Static Checking のチェックを有効にして静的解析を有効にします。そして、Check in Background のチェックを外します。多少ビルド時間がかかる弊害があるっちゃあるのですが、ここにチェック入ってるとVisual Studio のエラーと警告の所に出ませんので、いくらチェックしても無駄です。

次に Release 設定、自分は以下をお勧めしてます。

Perform Runtime Contract Checking にチェック、ドロップダウンでは Precondition、Only Public Surface で公開部分の呼出しについてチェックを有効にします。

こんぐらいが実行時パフォーマンスに影響を与えず、本来 ArgumentExceptionが飛ぶべき時に飛んでくれるとかの最低限のラインだと思います。

んでオモムロにビルドすると CLR4 なプロジェクトでは結構色々警告されると思います。これは .NET Framework 4の各種アセンブリには Code Contracts の契約情報がデフォルトで埋め込まれてるので .NET Framework コンポーネントを普通に使ってるところで変なパラメータを渡してると契約にマッチしてないよと確認してもらえるからです。よーするにCode Contracts有効にしてる静的チェックを有効にすると ArgumentNullException が飛んでくるようなコードは警告が出ます。デバッガなんて必要ナッシング。

これが思わぬバグを見つける事は良くあります。

自分のバグは恥ずかしいので他人のバグという卑怯な振る舞いしますが WCF で XML-RPC を扱うサンプルを MS の中の人が書いているんですが ( XML-RPC with WCF (Updated) ) Code Contract が以下の部分を警告します。

class XmlRpcDataContractSerializationHelper . Serialize

                else if (valueType == typeof(Stream))
                {
                    int chunkSize = 1024 * 5;
                    byte[] buffer = new byte[chunkSize];
                    int offset = 0;
                    int bytesRead;
                    writer.WriteStartElement(XmlRpcProtocol.ByteArray);
                    do
                    {
// CodeContracts: requires unproven:  count <= (buffer.Length – offset)    
                        bytesRead = ((Stream)value).Read(buffer, offset, buffer.Length);     
                        writer.WriteBase64(buffer, 0, bytesRead);
                        offset += bytesRead;
                    }
                    while (bytesRead == buffer.Length);
                    writer.WriteEndElement();
                }

どんなバグかわかります?

よくやりがちなんですが、Stream.Read の offset パラメータは、ストリームのオフセットじゃなく、格納先バッファのオフセットです。これを間違えている事がこの警告の原因です。offset でなく0を与えればいいわけですね。(そうすると offset を誰も使いやしねーよって ReSharper が言ってくれるので、offset 変数とその操作をまるまる消す事でこのバグが解消します)

どう?すごいでしょ?僕はコードを動かしてテストでバグを探すなんて事を全くしてないわけです。でもバグを発見できるし直すこともできます。Code Contracts を有効にするだけでバグったコードを書くと警告してくれるわけです。いまデバッガ叩きながら必死にデバッグしてるそこのあなた!Code Contractsの静的解析通してみたら「そのバグの原因ここよ!」が一発でわかるかもしれませんですよ。

 

んで、Code Contracts を有効にするとフレームワーク呼出しのこの警告をまず消す事になるんですが、基本的には Contract.Assert で警告された事をまず書くだけで消えます。Contract.Assert( hoge!=null ); とかで null じゃない事を確認してあげれば良いわけです。これをやるときにあからさまにオカシイ事やってると普通の人は気付きますよね。これが Code Contractsの効果です。デバッグ版でテストを走らせれば該当部分を通ればきっと Assert されるでしょう。

Assertの場合には実際に確認のコードが生成されます。確認処理が重くなりかねない場合などは Contract.Assume を使う事でここではこうなってる「はず!」と言い聞かせる事ができ、これで警告は消えますが、その「はず!」が満たされてる事はテストなりなんなりでちゃんと確認した方が良いでしょうね。

もちろんパラメータで受け取ったものとかを AssertやAssumeするのはおかしな話で事前条件として Contract.Requires で書いた方がいいでしょう。

また、「var x = 自分で作ったメソッド(); FrameworkMethod(x) 」という風に自分のメソッドの戻り値を Contract.Ensure してあげれば良いわけですね。

という訳で Ensure が出てきました。戻り値に対する Contract.Ensure はちょっと特殊な書き方をします。

Contract.Ensures(Contract.Result<T>()!=null)

このように Contract.Result() に対して条件を記述します。Ensureはメソッド内のどこに書いても構いませんがメソッドからの戻り時にこの条件がチェックされます。

既存コードの警告つぶしをやってると大抵は Contract の書き方に慣れます、そこから interface に対する契約とか、設計での活用に進むと良いでしょう。

という訳で「僕と契約しないか?」な Code Contracts の紹介でした。次回は Contracts に絡めて Pex を使ってコードカバレッジの高いテストの自動生成です。