Wie frei kann ich in einem Objektinvarianten im Code sein?

Question

Ich versuche, Invarianten in Codeverträgen zu demonstrieren, und ich dachte, ich würde ein Beispiel für eine sortierte Liste von Strings geben. Es unterhält intern ein Array mit Ersatzplatz für Ergänzungen usw. - genau wie List<T>, Grundsätzlich. Wenn es ein Element hinzufügen muss, fügt es ihn in das Array ein usw. Ich dachte, ich hätte drei Invarianten:

• Die Anzahl muss sinnvoll sein: nicht negativ und höchstens so groß wie die Puffergröße
• Alles im nicht verwendeten Teil des Puffers sollte null sein
• Jeder Artikel im verwendeten Teil des Puffer

Jetzt habe ich versucht, das auf diese Weise zu implementieren:

[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);
    }
}

Leider, ccrewrite durcheinander bringen die Schleifen.

Die Benutzerdokumentation besagt, dass die Methode nur eine Reihe von Aufrufen sein sollte Contract.Invariant. Muss ich den Code wirklich als so etwas umschreiben?

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));

Das ist etwas hässlich, obwohl es funktioniert. (Es ist viel besser als mein vorheriger Versuch, wohlgemerkt.)

Sind meine Erwartungen unangemessen? Sind meine Invarianten unangemessen?

(Fragte auch als als Frage im Code Contracts Forum. Ich werde hier selbst relevante Antworten hinzufügen.)

Answer 1

Von den (vorläufigen) MSDN -Seiten sieht es aus wie das Vertrag. FORALL -Mitglied kann Ihnen bei den 2 Reichweite Verträgen helfen. Die Dokumentation ist jedoch nicht sehr explizit über ihre Funktion.

//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

(Ich werde Henks Antwort akzeptieren, aber ich denke, es lohnt sich, dies hinzuzufügen.)

Die Frage wurde nun auf die beantwortet MSDN Forum, und das Ergebnis ist, dass die erste Form nicht erwartet zu arbeiten. Invarianten müssen wirklich, wirklich eine Reihe von Aufrufen sein Contract.Invariant, und das ist alles.

Dies macht es für den statischen Checker machbarer, die Invariante zu verstehen und ihn durchzusetzen.

Diese Einschränkung kann umgangen werden, indem einfach die gesamte Logik in ein anderes Mitglied eingebracht wird, z. B. ein IsValid Eigenschaft und dann anrufen:

Contract.Invariant(IsValid);

Das würde den statischen Checker zweifellos durcheinander bringen, aber in einigen Fällen kann es in einigen Fällen eine nützliche Alternative sein.

Answer 3

Erfinden die Designer das Rad nicht ein bisschen neu?

Was war los mit dem gute alte

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

?

Jetzt in C# haben wir keine const, aber warum kannst du nicht einfach ein definieren Invariant Funktion

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

Und dann einfach die Codeverträge in Bezug auf diese Funktion verwenden?

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

Vielleicht schreibe ich Unsinn, aber selbst in diesem Fall wird es einen didaktischen Wert haben, wenn mir jeder falsch sagt.