Unproven Stellen Sie sicher, dass in Verbindung mit einer Schnittstelle auf eine andere Eigenschaft verwiesen wird

Nehmen Sie den folgenden Code an:

Die Verträge versuchen zu sagen:

1. IsFooSet gibt true zurück, wenn Foo nicht null .
ist
2. Foo gibt null nicht zurück, wenn IsFooSet true zurückgibt.

Das funktioniert fast.
Allerdings bekomme ich eine "garantiert unbewiesen" auf return _foo; , weil der Prüfer nicht erkennt, dass Foo immer gleich _foo ist.

Das Ändern von Foo in eine automatische Eigenschaft mit einem private Setter entfernt diese Warnung, aber ich möchte das nicht tun (ich mag keine automatischen Eigenschaften mit privaten Sätzen).

Was muss ich im obigen Code ändern, damit die Warnung verschwindet und gleichzeitig das Feld _foo beibehalten wird?

Folgendes funktioniert nicht:

1. Änderung von IsFooSet zur Verwendung von _foo anstelle von Foo . Es wird eine zusätzliche "garantiert unbewiesen" auf IsFooSet ergeben.
2. Hinzufügen einer invarianten Foo == _foo . Dies führt zu einer "unveränderten Invariante" für den impliziten Standardkonstruktor. Darüber hinaus wird auf einer realen Code-Basis die Verarbeitungszeit des statischen Checkers um Größenordnungen höher sein.
3. Hinzufügen von Contract.Ensures(Contract.Result<string>() == _foo); zum Getter von Foo gemäß diese Antwort ändert nichts.