2015-02-08 18 views
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; 
    } 
} 

現在我需要補充的是指定InstanceOfFooInstanceOfBar是互相排斥的一類不變法:既可以null,但只有其中一個可以比null以外的東西。

我該如何在代碼中表達?

[ContractInvariantMethod] 
private void ObjectInvariant() 
{ 
    // How do I complete this invariant method? 
    Contract.Invariant((this.InstanceOfFoo == null && this.InstanceOfBar == null) || ...); 
} 

回答

1

看起來簡單還是應該enougth:

Contract.Invariant(this.InstanceOfFoo == null || this.InstanceOfBar == null); 

證明(對於某人來說,誰downvoted :)

1. (null, null): true || true -> true 
2. (inst, null): false || true -> true 
3. (null, inst): true || false -> true 
4. (inst, inst): false || false -> false 
+0

你能翻譯,爲簡單易懂的英語?當我嘗試總結符合本合同的所有可能配置時,我的腦子很痛。 – 2015-02-08 11:20:01

+0

@StevenLiekens請參閱我的更新與證明表 – 2015-02-08 11:21:45

+0

謝謝!我喜歡你如何佈置證明。我需要開始這樣做。 – 2015-02-08 11:34:44