Comment est-ce que je peux être libre dans le code d'un objet invariant?

Question

J'essaie de démontrer les invariants dans les contrats de code, et j'ai pensé donner un exemple de liste de chaînes triée. Il maintient un tableau en interne, avec un espace libre pour les ajouts etc - tout comme List<T>, fondamentalement. Quand il a besoin d'ajouter un élément, il insère dans le tableau, etc. je me suis dit que j'avais trois invariants:

• Le nombre doit être raisonnable: non négatif et au plus aussi grand que la taille du tampon
• Tout dans la partie inutilisée de la mémoire tampon doit être nul
• Chaque élément de la partie utilisée du tampon doit être au moins aussi « grand » comme l'élément avant qu'il

maintenant, j'ai essayé de mettre en œuvre de cette façon:

[ContractInvariantMethod] 
private void ObjectInvariant() 
{ 
    Contract.Invariant(count >= 0 && count <= buffer.Length); 
    for (int i = count; i < buffer.Length; i++) 
    { 
     Contract.Invariant(buffer[i] == null); 
    } 
    for (int i = 1; i < count; i++) 
    { 
     Contract.Invariant(string.Compare(buffer[i], buffer[i - 1]) >= 0); 
    } 
} 

Malheureusement, ccrewrite désorganise les boucles.

La documentation de l'utilisateur indique que la méthode doit simplement être une série d'appels à Contract.Invariant. Dois-je vraiment réécrire le code comme quelque chose comme ça?

Contract.Invariant(count >= 0 && count <= buffer.Length); 
Contract.Invariant(Contract.ForAll 
    (count, buffer.Length, i => buffer[i] == null)); 
Contract.Invariant(Contract.ForAll 
    (1, count, i => string.Compare(buffer[i], buffer[i - 1]) >= 0)); 

C'est un peu moche, même si cela fonctionne. (C'est beaucoup mieux que ma précédente tentative, attention à vous.)

Mes attentes sont-elles déraisonnables? Mes invariants sont-ils déraisonnables?

(également demandé comme question in the Code Contracts forum. Je vais ajouter des réponses pertinentes ici moi-même.)

Answer 1

Dans les pages MSDN (préliminaires), il semble que la députée Contract.ForAll pourrait vous aider avec les 2 contrats de gamme. La documentation n'est cependant pas très explicite sur sa fonction.

//untested 
Contract.Invariant(Contract.ForAll(count, buffer.Length, i => buffer[i] == null)); 
Contract.Invariant(Contract.ForAll(1, count, 
    i => string.Compare(buffer[i], buffer[i - 1]) >= 0)); 

Answer 2

(Je vais accepter la réponse de Henk, mais je pense qu'il vaut la peine d'ajouter ceci.)

La question a été répondu à la MSDN forum, et le résultat est que la première forme ISN 't devrait fonctionner. Invariants vraiment, vraiment besoin d'être une série d'appels à Contract.Invariant, et c'est tout. Cela permet au vérificateur statique de mieux comprendre l'invariant et de l'appliquer.

Cette restriction peut être contournée en plaçant simplement toute la logique dans un élément différent, par ex. une propriété IsValid, puis appeler:

Contract.Invariant(IsValid); 

qui ne mess doute le vérificateur statique, mais dans certains cas, il peut être une alternative utile dans certains cas.

Answer 3

Les concepteurs ne réinventent-ils pas un peu la roue?

Quel était le problème avec le good old

bool Invariant() const; // in C++, mimicking Eiffel 

?

Maintenant en C# nous n'avons pas const, mais pourquoi ne peut vous définir simplement une fonction Invariant

private bool Invariant() 
{ 
    // All the logic, function returns true if object is valid i.e. function 
    // simply will never return false, in the absence of a bug 
} 
// Good old invariant in C#, no special attributes, just a function 

puis il suffit d'utiliser le code des marchés en termes de cette fonction?

[ContractInvariantMethod] 
private void ObjectInvariant() 
{ 
    Contract.Invariant(Invariant() == true); 
} 

Peut-être que j'écris un non-sens, mais même dans ce cas, il aura une valeur didactique quand tout le monde me dit de mal.