¿Cuán libre puedo estar en el código en un objeto invariante?

Question

Estoy tratando de demostrar invariantes en Contratos de código, y pensé que daría un ejemplo de una lista ordenada de cadenas. Mantiene una matriz internamente, con espacio adicional para adiciones, etc., al igual que List<T>, básicamente. Cuando se tiene que añadir un elemento, se inserta en la matriz, etc. pensé que tenía tres invariantes:

• El recuento debe ser sensible: no negativos y como máximo tan grande como el tamaño del búfer
• Todo en la parte no utilizada de la memoria intermedia debe ser nula
• Cada elemento de la parte utilizada de la memoria intermedia debe ser al menos tan "grande" como el tema antes de que

Ahora, he tratado de implementar eso de esta manera:

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

Desafortunadamente, ccrewrite está estropeando los bucles.

La documentación del usuario dice que el método debe ser simplemente una serie de llamadas al Contract.Invariant. ¿Realmente tengo que volver a escribir el código como algo así?

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

Eso es algo feo, aunque funciona. (Es mucho mejor que mi intento anterior, piénselo).

¿Mis expectativas son irrazonables? ¿Son mis invariantes irrazonables?

(también pidió como question in the Code Contracts forum. Voy a añadir respuestas pertinentes aquí mismo.)

Answer 1

Desde las páginas preliminares) (MSDN Parece que el miembro Contract.ForAll que podría ayudar con los 2 contratos de rango. Sin embargo, la documentación no es muy explícita sobre su función.

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

(Voy a aceptar la respuesta de Henk, pero creo que vale la pena añadir esta.)

La pregunta ahora ha sido contestada en la MSDN forum, y el resultado es que la primera forma ISN 't espera que funcione. Los invariantes realmente necesitan ser una serie de llamadas al Contract.Invariant, y eso es todo.

Esto hace que sea más factible para el verificador estático entender el invariante y aplicarlo.

Esta restricción se puede eludir simplemente poniendo toda la lógica en un miembro diferente, p. una propiedad IsValid y, a continuación, llamar a:

Contract.Invariant(IsValid); 

Eso sería sin duda el desastre de electricidad estática, pero en algunos casos puede ser una alternativa útil en algunos casos.

Answer 3

¿No están los diseñadores reinventando la rueda un poco?

Qué le pasaba a la good old

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

?

Ahora en C# pero aún no disponemos const, pero ¿por qué no puede usted acaba de definir una función 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 

y luego sólo tiene que utilizar los contratos de código en términos de esa función?

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

Tal vez estoy escribiendo tonterías, pero incluso en ese caso tendrá algún valor didáctico cuando todo el mundo dice que estoy equivocado.