Jak wolny mogę być w kodzie w niezmienniku obiektu?

Question

Próbuję zademonstrować niezmienniki w Code Contracts i pomyślałem, że podam przykład posortowanej listy ciągów znaków. Utrzymuje tablicę wewnętrznie, z dodatkową przestrzenią dla dodatków itp. - tak jak w zasadzie List<T>. Kiedy trzeba dodać element, to wstawia go do tablicy, itd. Pomyślałem, miałem trzy niezmienników:

• Ilość musi być rozsądne: nieujemne i co najwyżej tak duży jak rozmiar bufora
• Wszystko w niewykorzystanej części bufora powinna być zerowa
• Każda pozycja w używane części bufora powinna wynosić co najmniej jako „duży” jako elementu przed

teraz Próbowałam wdrożyć w ten sposób:

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

Niestety, ccrewrite psuje pętle.

Dokumentacja użytkownika mówi, że metoda powinna być po prostu serią połączeń z numerem Contract.Invariant. Czy naprawdę muszę przepisać kod jako coś takiego?

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

To trochę brzydkie, chociaż działa. (To znacznie lepsze niż moja poprzednia próba, pamiętajcie.)

Czy moje oczekiwania są nieuzasadnione? Czy moje niezmienniki są nierozsądne?

(poprosił także jako question in the Code Contracts forum. Dodam żadnych stosownych odpowiedzi tutaj sam.)

Answer 1

Z (wstępny) stronach MSDN wygląda jak członek Contract.ForAll mogłyby pomóc w umowach między 2. Dokumentacja nie jest jednak bardzo jednoznaczna co do jej funkcji.

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

(mam zamiar przyjąć odpowiedź Henk, ale myślę, że warto dodać to.)

Pytanie został odpowiedział na MSDN forum i Skutek jest taki, że pierwsza forma ISN "t oczekuje się, że zadziała. Niezmienniki naprawdę muszą być serią połączeń do Contract.Invariant i to wszystko.

To sprawia, że ​​sprawdzanie statyczne jest bardziej realistyczne w celu zrozumienia niezmiennika i jego egzekwowania.

Ograniczenia tego można obejść, umieszczając całą logikę w innym członku, np. własności IsValid, a następnie wywołanie:

Contract.Invariant(IsValid); 

To bez wątpienia bałagan kontrolujący statyczny, ale w niektórych przypadkach może być użyteczna alternatywa w niektórych przypadkach.

Answer 3

Czy projektanci nie wymyślają na nowo koła?

Co było nie tak z good old

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

?

Teraz w C# nie mamy const, ale dlaczego nie można po prostu zdefiniować Invariant funkcję

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 

a potem po prostu korzystać z umów kod w kategoriach tej funkcji?

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

Może piszę bzdury, ale nawet w tym przypadku będzie to miało jakąś wartość dydaktyczną, gdy każdy mówi mi źle.