Niepotwierdzone Upewnić się, że odwołuje się do innej właściwości w połączeniu z interfejsem

Question

Zakładamy następujący kod:

[ContractClass(typeof(ICC4Contract))] 
public interface ICC4 
{ 
    bool IsFooSet { get; } 
    string Foo { get; } 
} 

public class CC4 : ICC4 
{ 
    private string _foo; 

    public bool IsFooSet { get { return Foo != null; } } 

    public string Foo { get { return _foo; } } 
} 

[ContractClassFor(typeof(ICC4))] 
public abstract class ICC4Contract : ICC4 
{ 
    public bool IsFooSet 
    { 
     get 
     { 
      Contract.Ensures((Contract.Result<bool>() && Foo != null) 
          || !Contract.Result<bool>()); 
      return false; 
     } 
    } 

    public string Foo 
    { 
     get 
     { 
      Contract.Ensures((Contract.Result<string>() != null && IsFooSet) 
          || !IsFooSet); 
      return null; 
     } 
    } 
} 

Kontrakty próbują powiedzieć:

1. IsFooSet powróci true jeśli Foo nie jest null.
2. Foo nie zwraca null, jeśli IsFooSet zwraca true.

To prawie działa.
Jednak otrzymuję komunikat "gwarantuje, że nie został sprawdzony" na return _foo;, ponieważ kontroler nie zdaje sobie sprawy, że Foo będzie zawsze równy zawsze będzie równy .

Zmiana Foo na automatyczną właściwość z seterem private usuwa to ostrzeżenie, ale nie chcę tego robić (nie lubię automatycznych właściwości z ustawieniami prywatnymi).

Co muszę zmienić w powyższym kodzie, aby ostrzeżenie zniknęło z zachowaniem pola _foo?

Następujące nie działa:

1. Zmiana IsFooSet używać _foo zamiast Foo. Spowoduje to dodatkowe "zapewnia niepotwierdzone" na IsFooSet.
2. Dodawanie niezmiennika Foo == _foo. Spowoduje to "niezmienione niezmienione" na domyślnym, domyślnym konstruktorze. Co więcej, na podstawie rzeczywistych kodów czas przetwarzania statycznego kontrolera będzie wyższy o magnitudo.
3. Dodanie Contract.Ensures(Contract.Result<string>() == _foo); do pobierającego z Foo zgodnie z this answer nic nie zmienia.

Answer 1

Można użyć zwarcia uprościć stan, i że działa z jakiegoś powodu:

[ContractClassFor(typeof(ICC4))] 
public abstract class ICC4Contract : ICC4 
{ 
    public bool IsFooSet 
    { 
     get 
     { 
      Contract.Ensures(!Contract.Result<bool>() || Foo != null); 
      return false; 
     } 
    } 

    public string Foo 
    { 
     get 
     { 
      Contract.Ensures(!IsFooSet || Contract.Result<string>() != null); 
      return null; 
     } 
    } 
}