À quel point puis-je être gratuit dans le code dans un invariant d'objet?

Question

J'essaie de démontrer les invariants dans les contrats de code et je pensais donner un exemple de liste triée de chaînes. Il gère un tableau en interne, avec un espace disponible pour les ajouts, etc., exactement comme List<T>. Lorsqu'il doit ajouter un élément, il l'insère dans le tableau, etc. J'ai supposé que j'avais trois invariants:

• Le nombre doit être raisonnable: non négatif et au plus grand que la taille de la mémoire tampon
• Tout ce qui se trouve dans la partie non utilisée du tampon doit être nul
• Chaque élément de la partie utilisée de la mémoire tampon doit être au moins égal à & "grand &"; comme l'élément précédent

Maintenant, j'ai essayé de mettre en œuvre cela de cette manière:

[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 gâche les boucles.

La documentation utilisateur indique que la méthode doit simplement consister en une série d'appels à Contract.Invariant. Dois-je vraiment réécrire le code comme suit?

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, bien que cela fonctionne. (C'est beaucoup mieux que ma précédente tentative, remarquez.)

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

(a également demandé en tant que question sur le forum Code Contracts . J'y ajouterai moi-même les réponses pertinentes.)

Answer 1

D'après les pages (préliminaires) MSDN, il semble que le membre Contract.ForAll puisse vous aider avec les contrats à deux plages. 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 que cela vaut la peine d'ajouter ceci.)

La question a maintenant reçu une réponse sur Forum MSDN , et le résultat est que le premier formulaire n'est pas censé fonctionner. Les invariants doivent vraiment, vraiment, être une série d'appels à Contract.Invariant, et c'est tout.

Cela permet au vérificateur statique de comprendre l’invariant et de l’appliquer.

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

Contract.Invariant(IsValid);

Cela aurait sans doute gâché le vérificateur statique, mais dans certains cas, cela pourrait être une alternative utile dans certains cas.

Answer 3

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

Qu'est-ce qui n'allait pas avec le bon vieux

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

?

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

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

et ensuite simplement utiliser les contrats de code en termes de cette fonction?

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

Peut-être que j'écris des bêtises, mais même dans ce cas, cela aura une valeur didactique lorsque tout le monde me dira tort.