Code Contracts: statische Analyse kann postcondition nicht überprüfen

Hi,

Ich spiele gerade ein bisschen mit Code Contracts herum und habe ein kleines Problem mit der statischen Analyse. Gegeben folgende Klasse:

internal class Stream
{
  private Type type;

  public Stream(Type type)
  {
    Contract.Requires(type != null);
    this.type = type;
  }

  public Type Type
  {
    get
    {
      Contract.Ensures(Contract.Result<Type>() != null);
      return type;
    }
    set
    {
      Contract.Requires(value != null);
      type = value;
    }
  }
}

Meinem Verständnis nach kann type nie null werden. Trotzdem beschwert sich die statische Codeanalyse bei "return type":

CodeContracts: ensures unproven: Contract.Result<Type>() != null

Ich kann das ganze natürlich "reparieren", indem ich eine entsprechende Invariante hinzufüge:

internal class Stream
{
   ...
  [ContractInvariantMethod]
  private void ObjectInvariant()
  {
    Contract.Invariant(type != null);
  }
}

Damit kann die Postcondition dann statisch verifiziert werden.

Kann mich jemand erhellen, warum der Analyzer das ohne Invariante nicht verifizieren kann? Ist das ein grundsätzliches Problem des Analyzers oder by-design, oder übersehe ich etwas im Code?

Grüße,
Andre

Hallo,

nach meinem Verständnis ist das as-designed denn der satic checker kapiert nicht dass vorher der Ctor aufgerufen werden muss - er sieht nur die Property als solche und nicht im Kontext der Klasse. Daher ist die Abhilfe eben die ContractInvariantMethod.

mfG Gü

Danke für deine Antwort. Ich werde also wohl die Invarianten verwenden. Der IL rewriter scheint bei automatischen Properties übrigens relativ clever zu sein.

Aus

internal class Stream
{
...
  public Type Type
  {
    get;set;
  }
  
  [ContractInvariantMethod]
  private void ObjectInvariant()
  {
    Contract.Invariant(Type != null);
  }
}

Macht er (sinngemäß):

internal class Stream
{
..

  public Type Type
  {
    get { 
      Contracts.Ensure(Contracts.Result<Type>() != null); 
      return type; 
    }
    set { 
      Contracts.Require(value  != null); 
      type = value; 
    }
  }
...
}

Das heißt, anstatt alle Invarianten am Ende des getters und setters zu überprüfen, wird aus den Invarianten passende Pre- und Postconditions für die Property erzeugt, da bei den automatischen Properties eh nur ein Backingfield betroffen ist.

Grüße,
Andre

Ist das ein grundsätzliches Problem des Analyzers oder by-design, oder übersehe ich etwas im Code?

Das ist ein Feature 😉
Wenn jemand die Klasse im Nachhinein erweitern würde, könnte das das Ensures schnell verletzten.
Daher wird man auf diese Weise gezwungen, eine entsprechende Invariante zu formulieren.

Ein bisschen anders verhält es sich, wenn du type auch noch als readonly markierst - dann fällt es wirklich unter die Kategorie "by design".
Siehe hierzu auch: Code Contracts Forum: State of fields marked as readonly