詳解.NET 4.0代碼契約組件
代碼契約組件是對(duì).NET的重要補(bǔ)充,這次我們將提供更為詳細(xì)的內(nèi)容。
如果要在.NET 4.0發(fā)布之前使用代碼契約,我們可以在Visual Studio項(xiàng)目中引用程序集Microsoft.Contracts.dll,該程序集安裝在%PROGRAMFILES%/Microsoft/Contracts/PublicAssemblies目錄下。.NET 4.0會(huì)在mscorlib.dll中包含契約組件。我們可以指定契約驗(yàn)證,可在編譯時(shí)(靜態(tài))或在運(yùn)行時(shí)(動(dòng)態(tài))執(zhí)行校驗(yàn)。
契約包含幾種類型:前置條件(Preconditions)、后置條件(Postconditions)、對(duì)象不變量(Object Invariants)、斷言(Assertions)、假定(Assumptions)、量詞(Quantifiers)、接口契約(Interface Contracts)和抽象方法契約(Abstract Method Contracts)。
前置條件使用Contract.Requires()進(jìn)行定義,如果在編譯時(shí)使用了符號(hào)(Symbol)CONTRACTS_FULL或CONTRACTS_PRECONDITIONS,那么IL中就會(huì)包含其編譯結(jié)果。例如:
Contract.Requires( x ! = null ); |
如下所示,前置條件通常作為方法體中的參數(shù)驗(yàn)證,如下所示:
public Rational( int numerator, int denominator) { Contract.Requires( denominator ! = 0 ); this .numerator = numerator; this .denominator = denominator; } |
如果不符合Contract.Requires()指定的條件,就會(huì)調(diào)用Debug.Assert(false),然后調(diào)用Environment.FailFast()。如果不管在編譯時(shí)使用哪個(gè)符號(hào),您都希望程序集中包含前置條件,那么可以使用Contract.RequiresAlways()。
當(dāng)方法結(jié)束時(shí),后置條件表示其結(jié)果需要滿足的契約。它通過Contract.Ensures()方法指定,如下例所示:
public int Denominator { get { Contract.Ensures( Contract.Result() != 0 ); return this .denominator; } } |
雖然似乎在返回結(jié)果之前就指定了條件,實(shí)際它還是會(huì)在返回結(jié)果之后,調(diào)用者得到結(jié)果之前進(jìn)行驗(yàn)證。
對(duì)象不變量則為每個(gè)實(shí)例指定條件。
ContractInvariantMethod]protected void ObjectInvariant () { Contract. Invariant ( this .denominator ! = 0 ); } |
至于其他類型的契約,斷言表示為Contract.Assert(),假定則表示為Contract.Assume()。一個(gè)失敗的Assert()會(huì)調(diào)用Debug.Assert(false)。假定與運(yùn)行時(shí)斷言相似,不同之處在于靜態(tài)檢驗(yàn)的方式。假定用于指定“期望”應(yīng)該符合的條件,而由于某些限制,該條件無法得到編譯器的驗(yàn)證。
接口契約為接口指定條件。它們使用在關(guān)聯(lián)于接口的獨(dú)立類上,因?yàn)榻涌诜椒ㄖ荒苈暶?,而不能擁有方法體。對(duì)于抽象方法契約同樣如此。
以下為一個(gè)使用契約的類:
|
.NET契約類代碼示例 |
【編輯推薦】