.NET Framework 4でのコントラクトプログラミング

仕事の変化の問題と、良いオフィスで開発者として働きたいという欲求に直面して、私は、アーキテクチャ、設計、OOP、およびプラットフォームや言語に固有ではないその他の分野の知識が不足していることに気付きました。 個人的な経験に加えて、情報源は標準です-本とインターネット。



その頃には、リファクタリングに関するFowlerの本とGoFの本が読まれていました。 これらの本は私に多くを与えてくれ、非常に有用でしたが、OOPについてもっと基本的なものが欲しかったのです。 フォーラムを検索して、私が興味を持った本をいくつか見つけました。

Bertrand Meyer「ソフトウェアシステムのオブジェクト指向設計」

Grady Butch、オブジェクト指向分析および設計

バーバラ・リスコフ。 ソフトウェア開発での抽象化と仕様の使用



残念ながら、後者を電子形式で見つけることはできませんでした。また、紙ではどこを見ればいいのかさえわかりません。 当時の店内での存在感は、マイヤーの本でしかなかったので、それを受け取りました。



本について少し。



いくつかのニュアンスは残っていましたが、私は本が好きで、合理化され、たくさん説明されました。 全体として、翻訳は読み書き可能であり、技術と用語を知っている人々によって作成されました。 残念ながら、私はテキストを書く年を見つけませんでしたが、私が理解したように、90年代半ば頃。 これは主に、OOPが当時人気のあった他のアプローチよりも優れていると著者が熱心に主張している理由を説明しています。 私はいくつかの点が本当に好きではありませんでした。 最初に、関数型プログラミングに関するいくつかの否定性に多くの注意が払われます。 第二に、一般的に、本全体は、私には思われたように、「二つの意見、一つは私の意見、もう一つは間違っている」というスタイルで書かれていた。 著者は、本に記載されている原則に基づいたエッフェル語を作成しました。すべての論争と境界の決定は、著者に有利に解釈され、別のオプションのコメントをつぶします。 そのような「巨大な欠陥」のあるJavaおよびC#言語が一般的になった方法が理解できない場合があります。 ただし、ジェネリックはJavaと.Netの両方で非常に期待されていたことを認めなければなりません。



契約によるプログラミング。



本全体を通る赤い糸は、契約プログラミングのアイデアです。 各サブプログラム(メソッド)には、事前条件と事後条件があります。 前提条件は、プログラムが呼び出されるたびに実行する必要があるプロパティを設定します。 事後条件は、プログラムの完了時にプログラムによって保証されるプロパティを決定します。 事前条件と事後条件は、個々のプログラムのプロパティを記述します。 ただし、クラスインスタンスにはグローバルプロパティもあります。 これらはクラス不変式と呼ばれ、クラスを特徴付けるより深いセマンティックプロパティと整合性制約を定義します。 不変条件は前提条件と事後条件に追加されます。 契約プログラミングは、コードを文書化し、デバッグし、不要なチェックを排除するための優れた方法です。 たとえば、メソッドが非負の数を返すという事後条件で記述されている場合、平方根を抽出するときに非負の数をチェックする必要はありません。 これはすべて、信頼性、品質、開発速度の向上につながります。



残念ながら、.Net開発者は(自分の)仕事でこのアプローチを使用する機会を奪われました。 もちろんDebug.Assertを使用できますが、それは正しくありません。 アサートを使用すると、コードの特定のセクションに条件を設定できますが、事前条件と事後条件の代わりに使用できます。 ただし、すべてのクラスメソッドと、場合によっては子孫に設定されるクラス不変式がまだあります。



.Net framework 4.0の契約システムの一部。



契約システムは4つの主要部分で構成されています。 最初の部分はライブラリです。 契約は、mscorlib.dllアセンブリからのContractクラス(System.Diagnostics.Contracts名前空間)の静的メソッド呼び出しを使用してエンコードされます。 コントラクトは本質的に宣言的であり、メソッドの開始時のこれらの静的呼び出しはメソッドシグネチャの一部と見なすことができます。 属性は非常に制限されているため、これらはメソッドであり、属性ではありませんが、これらの概念は近いものです。

2番目の部分は、バイナリリライタccrewrite.exeです。 このツールは、MSILの指示を変更し、契約を検証します。 このツールは、コードのデバッグに役立つ契約の実行を確認する機会を提供します。 それがなければ、契約は単なるドキュメントであり、コンパイルされたコードには含まれません。

3番目の部分は、静的な検証ツールcccheck.exeです。このツールは、コードを実行せずに分析し、すべての契約が完了したことを証明しようとします。

4番目の部分はccrefgen.exeで、契約のみを含む別のアセンブリを作成します。



契約のライブラリ。 前提条件。



前提条件には3つの主要な形式があり、そのうち2つはContractクラスのRequiresメソッドに基づいています。 どちらのアプローチにもオプションがオーバーロードされており、契約違反の場合にメッセージを含めることができます。



public Boolean TryAddItemToBill(Item item)<br>{<br> Contract.Requires<NullReferenceException>(item != null );<br> Contract.Requires(item.Price >= 0);<br>} <br><br> * This source code was highlighted with Source Code Highlighter .







このメソッドは、メソッドを入力するときに必要なものを指定する簡単な方法です。 要求フォームを使用すると、契約違反の場合に例外をスローできます。



前提条件の3番目の形式は、if-then-throw構文を使用してパラメーターをテストすることです。



public Boolean ExampleMethod( String parameter)<br>{<br> if (parameter == null )<br> throw new ArgumentNullException( "parameter must be non-null" );<br>} <br><br> * This source code was highlighted with Source Code Highlighter .







このアプローチには、起動するたびに実行されるという利点があります。 ただし、契約システムにはさらに多くの機能(ツール、継承など)があります。 このコンストラクトをコントラクトに変換するには、Contract.EndContractBlock()メソッドへの呼び出しを追加する必要があります



public Boolean ExampleMethod( String parameter)<br>{<br> if (parameter == null )<br> throw new ArgumentNullException( "parameter must be non-null" );<br> // tells tools the if-check is a contract <br> Contract.EndContractBlock();<br>} <br><br> * This source code was highlighted with Source Code Highlighter .







if-then-throwコンストラクトはメソッドコード内で複数回発生する可能性がありますが、コンストラクトがメソッドを開始し、Contract.EndContractBlock()メソッドが呼び出された後のみ、このコードはコントラクトになります。



事後条件。



事後条件には2つのオプションがあります。1つ目は通常の戻りを保証し、2つ目は指定された例外をスローするときに何かを保証します。



public Boolean TryAddItemToBill(Item item)<br>{<br> Contract.Ensures(TotalCost >= Contract.OldValue(TotalCost));<br> Contract.Ensures(ItemsOnBill.Contains(item) || (Contract.Result<Boolean>() == false ));<br> Contract.EnsuresOnThrow<IOException>(TotalCost == Contract.OldValue(TotalCost))<br>}<br> <br><br> * This source code was highlighted with Source Code Highlighter .







2番目のオプション(説明用に作成)



public int Foo( int arg)

{

Contract.EnsuresOnThrow<DivideByZeroException>( false );

int i = 5 / arg;

return i;

}




* This source code was highlighted with Source Code Highlighter .








このメソッドにゼロを渡すと、契約に違反します。



メソッドの終了時に事後条件がチェックされます



public class ExampleClass<br>{<br> public Int32 myValue;<br> public Int32 Sum( Int32 value )<br> {<br> Contract.Ensures(Contract.OldValue( this .myValue) == this .myValue);<br> myValue += value ; // <br> return myValue;<br> }<br>}<br> <br> * This source code was highlighted with Source Code Highlighter .







不変量



不変式は、不変法を使用してエンコードされます。



public static void Invariant( bool condition);<br> public static void Invariant( bool condition, String userMessage); <br><br> * This source code was highlighted with Source Code Highlighter .







これらは、不変条件のみを含むクラスの単一のメソッドで宣言され、ContractInvariantMethod属性でマークされます。 伝統的に、このメソッドはObjectInvariantと呼ばれ、保護されているため、他の人のコードからこのメソッドを明示的に呼び出すことはできません。



[ContractInvariantMethod]<br> protected void ObjectInvariant()<br>{<br> Contract.Invariant(TotalCost >= 0);<br>}<br> <br> * This source code was highlighted with Source Code Highlighter .







コントラクトを使用したデバッグ。



デバッグにコントラクトを使用するためのいくつかの可能なシナリオがあります。 それらの1つは、静的分析および契約分析ツールの使用です。 2番目のオプションは、実行時チェックです。 それを最大限に活用するには、契約に違反したときに何が起こったかを知る必要があります。 ここでは、通知と反応の2つの段階を区別できます。

契約に違反すると、イベントが発生します。



public sealed class ContractFailedEventArgs : EventArgs <br>{<br> public String Message { get ; }<br> public String Condition { get ; }<br> public ContractFailureKind FailureKind { get ; }<br> public Exception OriginalException { get ; }<br> public Boolean Handled { get ; }<br> public Boolean Unwind { get ; }<br> public void SetHandled();<br> public void SetUnwind();<br> public ContractFailedEventArgs(ContractFailureKind failureKind,<br> String message, String condition, <br> Exception originalException);<br>} <br><br> * This source code was highlighted with Source Code Highlighter .







これはプレリリースであり、最終リリースで何かが変わる可能性があることを忘れないでください。

このイベントをロギングに使用できます。



テストフレームワークを使用する場合、次のようなことができます(Visual Studioフレームワークの例)



[AssemblyInitialize]<br> public static void AssemblyInitialize(TestContext testContext)<br>{<br> Contract.ContractFailed += (sender, eventArgs) =><br> {<br> eventArgs.SetHandled();<br> eventArgs.SetUnwind(); // cause code to abort after event <br> Assert.Fail(eventArgs.Message); // report as test failure <br> };<br>}<br> <br> * This source code was highlighted with Source Code Highlighter .







UPD





継承





コメントの多くは、Debug.Assertと単体テストとの類似点を見つけています。 元々のさまざまな目標に加えて、重要な違いは継承です。 契約は継承されます!

例、コンソールアプリケーション、



using System;

using System.Collections. Generic ;

using System.Linq;

using System.Text;

using System.Diagnostics.Contracts;



namespace ConsoleApplication1

{

class ClassWithContract

{

int intNotNegativeField;

[ContractInvariantMethod]

protected virtual void ObjectInvariant()

{

Contract.Invariant( this .intNotNegativeField >= 0);

}



public virtual int intNotNegativeProperty

{

get

{

return this .intNotNegativeField;

}

set

{

this .intNotNegativeField = value ;

}

}



public ClassWithContract()

{

}



}



class InheritFromClassWithContract : ClassWithContract

{



}

}



* This source code was highlighted with Source Code Highlighter .








およびprogramm.csコード



using System;

using System.Collections. Generic ;

using System.Linq;

using System.Text;



namespace ConsoleApplication1

{

class Program

{

static void Main( string [] args)

{

InheritFromClassWithContract myObject = new InheritFromClassWithContract();

myObject.intNotNegativeProperty = -3;



}

}

}



* This source code was highlighted with Source Code Highlighter .








この例では、契約に違反します。 増幅緩和条件も考慮されます。 Meyerによれば、相続人は前提条件を弱め(より多くのオプションを受け入れる)、後条件を強化する権利を持ち、戻り値をさらに制限します。

これは、動的バインディングと多態性を考えると自然です。



この記事は、Melitta Andersenによる記事(略語付きの無料翻訳) コード契約に基づいています。



関連リンク。




All Articles