Quanto posso essere libero nel codice in un oggetto invariante?

Question

Sto cercando di dimostrare gli invarianti nei Contratti di codice e ho pensato di fare un esempio di un elenco ordinato di stringhe. Mantiene un array internamente, con spazio libero per aggiunte ecc., Proprio come List<T>, in pratica. Quando deve aggiungere un elemento, lo inserisce nella matrice, ecc. Ho pensato di avere tre invarianti:

• Il conteggio deve essere ragionevole: non negativo e al massimo grande quanto la dimensione del buffer
• Tutto nella parte inutilizzata del buffer deve essere nullo
• Ogni elemento nella parte usata del buffer dovrebbe essere almeno come " big " come l'elemento precedente

Ora, ho provato a implementarlo 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 sta incasinando i loop.

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

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

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

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

(Richiesto anche come domanda nel forum Contratti di codice . Aggiungerò qui le risposte pertinenti.)

Answer 1

Dalle pagine (preliminari) di MSDN sembra che il contratto.Per tutti i membri potrebbero aiutarti con i contratti a 2 intervalli. La documentazione non è molto esplicita sulla sua funzione però.

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

(Accetterò la risposta di Henk, ma penso che valga la pena aggiungerlo.)

La domanda è stata ora risolta in forum MSDN e il risultato è che il primo modulo non è dovrebbe funzionare. Gli invarianti devono davvero essere una serie di chiamate a Contract.Invariant, e questo è tutto.

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

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

Contract.Invariant(IsValid);

Ciò senza dubbio rovinerebbe il controllo statico, ma in alcuni casi potrebbe essere un'alternativa utile in alcuni casi.

Answer 3

I progettisti non stanno reinventando un po 'la ruota?

Cosa c'era di sbagliato nel buon vecchio

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

Ora in C # non abbiamo const, ma perché non puoi semplicemente definire una Invariant funzione

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 quindi utilizzare i Contratti di codice in termini di tale funzione?

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

Forse sto scrivendo sciocchezze, ma anche in quel caso avrà un valore didattico quando tutti mi diranno male.