¿Qué tan libre puedo ser en el código en un objeto invariante?

Question

Estoy intentando demostrar invariantes en contratos de código y pensé en dar un ejemplo de una lista ordenada de cadenas.Mantiene una matriz internamente, con espacio libre para adiciones, etc., tal como List<T>, básicamente.Cuando necesita agregar un elemento, lo inserta en la matriz, etc.Pensé que tenía tres invariantes:

• El conteo debe ser sensato:no negativo y como máximo tan grande como el tamaño del buffer
• Todo lo que esté en la parte no utilizada del buffer debe ser nulo.
• Cada elemento en la parte utilizada del buffer debe ser al menos tan "grande" como el elemento anterior.

Ahora, he intentado 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á arruinando los bucles.

La documentación del usuario dice que el método debería ser solo una serie de llamadas a Contract.Invariant.¿Realmente tengo que reescribir el código como algo como esto?

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, claro está).

¿Son mis expectativas irrazonables?¿Son mis invariantes irrazonables?

(También preguntado como pregunta en el foro de Contratos de Código.Agregaré aquí cualquier respuesta relevante).

Answer 1

De las páginas (preliminares) de MSDN parece que el miembro Contract.ForAll podría ayudarlo con los contratos de 2 rangos. 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 agregar esto).

La pregunta ya ha sido respondida en el foro de MSDN, y el resultado es que la primera forma no es se espera que funcione.Las invariantes realmente necesitan ser una serie de llamadas a Contract.Invariant, y eso es todo.

Esto hace que sea más factible que el verificador estático comprenda el invariante y lo aplique.

Esta restricción se puede eludir simplemente poniendo toda la lógica en un miembro diferente, por ejemplo.un IsValid propiedad, y luego llamando:

Contract.Invariant(IsValid);

Sin duda, eso arruinaría el verificador estático, pero en algunos casos puede ser una alternativa útil.

Answer 3

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

¿Qué estaba mal con el bien viejo

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

?

Ahora en C # no tenemos const, pero ¿por qué no puede simplemente definir una Invariant función

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 solo usa 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 todos me digan mal.