Code Contractsを使用した仕様記述の例（ジャンケン判定）

Code Contractsを使用した仕様記述の参考としてジャンケン判定の仕様記述の例をあげておきます。

    public enum Gesture
    {
        Rock,
        Scissors,
        Paper,
    }
    public enum Winner
    {
        Player1,
        Player2,
        Draw,
    }
    public class ScissorsPaperRock
    {
        public Winner Judge(Gesture player1, Gesture player2)
        {
            // 事前条件
            Contract.Requires(
                    (player1 == Gesture.Rock)
                    ||
                    (player1 == Gesture.Scissors)
                    ||
                    (player1 == Gesture.Paper)
                );
            Contract.Requires(
                    (player2 == Gesture.Rock)
                    ||
                    (player2 == Gesture.Scissors)
                    ||
                    (player2 == Gesture.Paper)
                );

            // 事後条件
            Contract.Ensures(
                    ( // Player1の勝ち
                        (
                            (
                                (Contract.OldValue<Gesture>(player1) == Gesture.Scissors)
                                &&
                                (Contract.OldValue<Gesture>(player2) == Gesture.Paper)
                            )
                            ||
                            (
                                (Contract.OldValue<Gesture>(player1) == Gesture.Rock)
                                &&
                                (Contract.OldValue<Gesture>(player2) == Gesture.Scissors)
                            )
                            ||
                            (
                                (Contract.OldValue<Gesture>(player1) == Gesture.Paper)
                                &&
                                (Contract.OldValue<Gesture>(player2) == Gesture.Rock)
                            )
                        )
                        &&
                        (Contract.Result<Winner>() == Winner.Player1)
                    )
                    ||
                    ( // Player2の勝ち
                        (
                            (
                                (Contract.OldValue<Gesture>(player1) == Gesture.Paper)
                                &&
                                (Contract.OldValue<Gesture>(player2) == Gesture.Scissors)
                            )
                            ||
                            (
                                (Contract.OldValue<Gesture>(player1) == Gesture.Scissors)
                                &&
                                (Contract.OldValue<Gesture>(player2) == Gesture.Rock)
                            )
                            ||
                            (
                                (Contract.OldValue<Gesture>(player1) == Gesture.Rock)
                                &&
                                (Contract.OldValue<Gesture>(player2) == Gesture.Paper)
                            )
                        )
                        &&
                        (Contract.Result<Winner>() == Winner.Player2)
                    )
                    ||
                    ( // あいこ
                        (Contract.OldValue<Gesture>(player1) == Contract.OldValue<Gesture>(player2))
                        &&
                        (Contract.Result<Winner>() == Winner.Draw)
                    )
                );

            // 実装
            return default(Winner); // dummy return
        }
    }

これでScissorsPaperRockクラスのJudgeメソッドでPexを実行するとこの仕様記述のカバレッジ100%となるテストを自動生成して実行してくれることを確認することができます。
この例だけでは分かりにくいですが、複数のメソッドやクラスが関係する場合にもCode Contractsの静的検証で「Code Contracts（契約）の使いどころ - Jamzzの日々」に書いた継承の例で示したようにメソッド呼び出し元のコンテキストにおける複数メソッド呼び出しについてもその整合性を検証してくれますし、さらに任意のコンテキスト（メソッド）でPexを実行すればカバレッジ100%の動的検証により論理的な整合性の検証ができると思います。