自動實現的屬性上的代碼合同

Question

有沒有什麼辦法可以將自動實現的屬性放在.NET中？ （以及如果答案是'是'）？

（我假設使用從DevLabs .NET代碼合同）

Answer 1

謝謝Porges。

我的錯誤是，我實際使用ReleaseRequires選項，這，的確，只有涉及通用版本的方法，Requires<T>的。

置於自動執行屬性上的不變量是確實變成了Requires前提條件，但它不是通用的 - 這就是爲什麼它不能使用此選項。

怎麼辦：

• VARIANT 1.考慮使用代碼段和可愛Requires<T>，而不是自動實現的屬性 - 這使我們能夠使用所需類型的異常。

• VARIANT 2. 更改代碼契約的選項的ReleaseRequires到Preconditions和隨意寫上自動性能不變 - 重寫器工具會自動改變他們進入Requires。但是，它們將是非通用的 - 這意味着，如果合同被破壞，將會引發ContractException，並且無法更改此行爲。

謝謝大家的幫助！

Answer 2

我想不會，但你可以很容易地編寫代碼，可將做到這一點。如果你走這條路線，here is a free snippet editor這將使任務非常容易。

Answer 3

是的，這是可能的 - 所有這一切都需要的是你的合同條件添加到[ContractInvariantMethod]方法在你的類，然後添加相當於Requires前提，以自動set之三，和一個後置條件Ensures被添加到get。從的Reference

作爲示例示出第2.3.1節，在自動性質不變量變成：

1. 甲前提條件設置器
2. 一種用於吸氣劑的後置條件
3. 的不變的基礎支持領域

並通過例如：

public int MyProperty { get; private set ;} 

[ContractInvariantMethod] 
private void ObjectInvariant() 
{ 
    Contract.Invariant (this.MyProperty >= 0); 
} 

「等同於下面的代碼：」

private int backingFieldForMyProperty; 
public int MyProperty 
{ 
    get 
    { 
    Contract.Ensures(Contract.Result<int>() >= 0); 
    return this.backingFieldForMyProperty; 
    } 

    private set 
    { 
    Contract.Requires(value >= 0); 
    this.backingFieldForMyProperty = value; 
    } 
} 

[ContractInvariantMethod] 
private void ObjectInvariant() 
{ 
    Contract.Invariant (this.backingFieldForMyProperty >= 0); 
...