Quanto posso essere libero nel codice in un oggetto invariante?

Question

Sto provando a dimostrare le invarianti nei Contratti di codice e ho pensato di fornire un esempio di elenco ordinato di stringhe. Mantiene una matrice internamente, con spazio libero per aggiunte ecc. - come List<T>, in pratica. Quando è necessario aggiungere un elemento, inserisce nella matrice, ecc ho pensato che avevo tre invarianti:

• Il conteggio deve essere sensibile: non negativi e al più grande come la dimensione del buffer
• Tutto in parte non utilizzata del buffer dovrebbe essere nullo
• Ogni elemento della parte usata del tampone dovrebbe essere almeno come "grande" come la voce prima che

Ora, ho cercato di implementalo in questo modo:

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

Sfortunatamente, ccrewrite si incasina negli anelli.

La documentazione dell'utente dice che il metodo dovrebbe essere solo una serie di chiamate a Contract.Invariant. Devo davvero riscrivere il codice come qualcosa di simile?

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

Questo è un po 'brutto, anche se funziona. (È molto meglio del mio precedente tentativo, intendiamoci).

Le mie aspettative sono irragionevoli? I miei invarianti sono irragionevoli?

(anche chiesto come question in the Code Contracts forum. Io aggiungo risposte rilevanti qui me stesso.)

Answer 1

Dalle (preliminari) pagine MSDN sembra che il membro Contract.ForAll potrebbe aiutare con i contratti di 2 gamma. La documentazione però non è molto esplicita sulla sua funzione.

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

(ho intenzione di accettare la risposta di Henk, ma penso che valga la pena di aggiungere questo.)

La questione è stata ora risolta sulla MSDN forum, e il risultato è che la prima forma isn 't dovrebbe funzionare. Gli invarianti hanno davvero bisogno di essere una serie di chiamate allo Contract.Invariant, e questo è tutto.

Ciò rende più fattibile per il controllore statico capire l'invariante e applicarlo.

Questa limitazione può essere aggirata semplicemente mettendo tutta la logica in un membro diverso, ad es. una proprietà IsValid, e quindi chiamando:

Contract.Invariant(IsValid); 

che avrebbe senza dubbio rovinare il controllo statico, ma in alcuni casi può essere una valida alternativa in alcuni casi.

Answer 3

I progettisti non reinventano un po 'la ruota?

Cosa c'era di sbagliato con il good old

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

?

Ora in C# che non hanno const, ma perché non si può solo definire una funzione di 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 

e poi basta utilizzare i contratti di codice in termini di quella funzione?

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

Forse sto scrivendo una sciocchezza, ma anche in quel caso si avrà qualche valore didattico quando tutti mi dice male.