Wie frei kann ich im Code in einer Objektinvariante sein?

Question

Ich versuche, Invarianten in Code Contracts zu demonstrieren, und ich dachte, ich würde ein Beispiel für eine sortierte Liste von Zeichenfolgen geben. Es verwaltet ein Array intern, mit Platz für Ergänzungen usw. - genau wie List<T>, im Grunde genommen. Wenn es ein Element hinzugefügt werden muss, es fügt sie in das Array, etc. Ich dachte, ich drei Invarianten hatte:

• Der Graf muss sinnvoll sein: nicht-negativ und höchstens so groß wie die Puffergröße
• Alles in dem ungenutzten Teil des Puffers sollte im Altteil des Puffers sollte mindestens so „groß“ wie das Element sein, bevor es

Jetzt

Jeden Punkt null sein, ich habe versucht, Implementieren Sie das auf diese Weise:

[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 ist die Schleifen durcheinander.

Die Benutzerdokumentation sagt, dass die Methode sollte nur eine Reihe von Anrufen zu Contract.Invariant sein. Muss ich den Code wirklich so 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 früherer Versuch, wohlgemerkt.)

Sind meine Erwartungen unvernünftig? Sind meine Invarianten unvernünftig?

(auch gefragt, als question in the Code Contracts forum. Ich alle relevanten Antworten uns hier hinzufügen würde.)

Answer 1

Aus den (vorläufigen) MSDN-Seiten es wie das Contract.ForAll Mitglied sieht, könnte man mit den 2 Bereich Verträgen helfen. Die Dokumentation ist 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 Henk Antwort akzeptieren, aber ich denke, dass es sich lohnt, diese hinzuzufügen.)

Die Frage ist nun auf der MSDN forum beantwortet wurde, und das Ergebnis ist, dass die erste Form isn 't erwartet zu arbeiten. Invarianten müssen wirklich, wirklich eine Reihe von Anrufen an sein, und das ist alles.

Dies macht es möglich, für die statischen checker der unveränderlichen und durchzusetzen, sie zu verstehen.

kann diese Einschränkung, indem man einfach die gesamte Logik in ein anderes Mitglied umgangen werden, z.B. eine IsValid Eigenschaft, und dann ruft:

Contract.Invariant(IsValid); 

, dass der statische checker, keinen Zweifel vermasseln würde, aber in einigen Fällen kann es eine sinnvolle Alternative in einigen Fällen sein.

Answer 3

Sind nicht die Designer das Rad ein bisschen neu zu erfinden?

Was war falsch mit dem good old

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

?

Jetzt in C# wir haben const nicht, aber warum können Sie nicht nur eine 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 den Code Verträge in Bezug auf diese Funktion nutzen definieren?

Vielleicht schreibe ich Unsinn, aber selbst in diesem Fall wird es einen didaktischen Wert haben, wenn alle mich falsch verstehen.