1
我的類有兩個私有字段和三個構造函數。對於互斥條件的類不變式
一個構造函數是不分配任何值的默認構造函數。
其餘構造每個實例化兩個領域之一,以確保一個領域是總是null
和其他領域是從未null
。
public class MyClass
{
private readonly Foo foo;
public Foo InstanceOfFoo { get { return this.foo; } }
private readonly Bar bar;
public Bar InstanceOfBar { get { return this.bar; } }
// Default constructor: InstanceOfFoo == null & InstanceOfBar == null
public MyClass()
{
}
// Foo constructor: InstanceOfFoo != null & InstanceOfBar == null
public MyClass(Foo foo)
{
Contract.Requires(foo != null);
this.foo = foo;
}
// Bar constructor: InstanceOfFoo == null & InstanceOfBar != null
public MyClass(Bar bar)
{
Contract.Requires(bar != null);
this.bar = bar;
}
}
現在我需要補充的是指定InstanceOfFoo
和InstanceOfBar
是互相排斥的一類不變法:既可以null
,但只有其中一個可以比null
以外的東西。
我該如何在代碼中表達?
[ContractInvariantMethod]
private void ObjectInvariant()
{
// How do I complete this invariant method?
Contract.Invariant((this.InstanceOfFoo == null && this.InstanceOfBar == null) || ...);
}
你能翻譯,爲簡單易懂的英語?當我嘗試總結符合本合同的所有可能配置時,我的腦子很痛。 – 2015-02-08 11:20:01
@StevenLiekens請參閱我的更新與證明表 – 2015-02-08 11:21:45
謝謝!我喜歡你如何佈置證明。我需要開始這樣做。 – 2015-02-08 11:34:44