Limitations de vérification statique lors de l'utilisation de fonctions pures dans les contrats de code C#?

Question

J'essaie de vérifier statiquement l'implémentation partielle suivante d'une pile basée sur un tableau avec des contrats de code. La méthode Pop() utilise la fonction pure IsNotEmpty() pour garantir que l'accès au tableau suivant sera égal ou supérieur à la limite inférieure. Le vérificateur statique échoue et suggère que j'ajoute la condition préalable Contract.Requires(0 <= this.top).

Quelqu'un peut-il expliquer pourquoi le vérificateur ne peut pas prouver que l'accès au réseau est valide par rapport à la borne inférieure donnée au contrat IsNotEmpty()?

Au début, je pensais que l'approche Contract.Requires(IsNotEmpty()) pourrait être incorrecte, car une sous-classe pourrait remplacer IsNotEmpty(). Cependant, le vérificateur ne peut toujours pas prouver que l'accès au tableau est valide si je marque la classe sealed.

Mise à jour: Si je remplace IsNotEmpty() par une propriété en lecture seule, la vérification aboutit comme prévu. Cela soulève la question: comment/pourquoi les propriétés en lecture seule et les fonctions pures sont traitées différemment?

class StackAr<T> 
{ 
    private T[] data; 
    private int capacity; 

    /// <summary> 
    /// the index of the top array element 
    /// </summary> 
    private int top; 

    [ContractInvariantMethod] 
    private void ObjectInvariant() 
    { 
     Contract.Invariant(data != null); 
     Contract.Invariant(top < capacity); 
     Contract.Invariant(top >= -1); 
     Contract.Invariant(capacity == data.Length); 
    } 

    public StackAr(int capacity) 
    { 
     Contract.Requires(capacity > 0); 
     this.capacity = capacity; 
     this.data = new T[capacity]; 
     top = -1; 
    } 

    [Pure] 
    public bool IsNotEmpty() 
    { 
     return 0 <= this.top; 
    } 

    public T Pop() 
    { 
     Contract.Requires(IsNotEmpty()); 

     //CodeContracts: Suggested precondition: 
     //Contract.Requires(0 <= this.top); 

     T element = data[top]; 
     top--; 
     return element; 
    } 
} 

Answer 1

Cela devrait résoudre le problème:

[Pure] 
public bool IsNotEmpty() { 
    Contract.Ensures(Contract.Result<bool>() && 0 <= this.top || !Contract.Result<bool>() && 0 > this.top); 
    return 0 <= this.top; 
} 

Voir ce fil sur les contrats de code forum pour plus d'informations: Calling a method in Contract.Requires

Edit:

Une autre solution à ce problème, comme mentionné dans le fil lié ci-dessus, est le -infer option de ligne de commande:

Maintenant, déduisant la condition post de cette méthode est possible, et en fait, nous avons la possibilité de le faire: essayez d'ajouter -infer assure sur la ligne supplémentaire d'options dans la propriété du contrat volet pour le vérificateur statique.

J'ai vérifié, et cela résout le problème. Si vous regardez dans le code contracts manual, vous verrez que l'option par défaut est d'inférer uniquement les post-conditions de propriété. En utilisant ce commutateur, vous pouvez le dire à tenter de déduire les post-conditions de méthodes aussi:

-infer (nécessite + propertyensures + methodensures) (par défaut = propertyensures)