.net 4.0 - google - ¿Qué tan libre puedo estar en el código en un objeto invariante?

meta tags google

Question

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

• El recuento debe ser sensible: no negativo y, a lo sumo, tan grande como el tamaño del búfer
• Todo en la parte no utilizada del búfer debe ser nulo.
• Cada elemento en la parte utilizada del búfer debe ser al menos tan "grande" como el elemento anterior.

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á arruinando los bucles.

La documentación del usuario dice que el método debe ser solo una serie de llamadas a Contract.Invariant . ¿Realmente tengo que reescribir 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, fíjate.)

¿Mis expectativas son irrazonables? ¿Mis invariantes son irrazonables?

(También formulada como una pregunta en el foro de Contratos de Código . Agregaré las respuestas relevantes aquí mismo).

Answer 1

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

Lo que estaba mal con el viejo

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

?

Ahora en C # no tenemos const, pero ¿por qué no puedes simplemente 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 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.

Answer 2

(Voy a aceptar la respuesta de Henk, pero creo que vale la pena agregar esto).

La pregunta ahora ha sido respondida en el foro de MSDN , y el resultado es que no se espera que el primer formulario funcione. Los 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 lo invariable y lo aplique.

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

Contract.Invariant(IsValid);

Eso sin duda arruinaría el comprobador estático, pero en algunos casos puede ser una alternativa útil en algunos casos.

Answer 3

Desde las páginas (preliminares) de MSDN, parece que el miembro Contract.ForAll podría ayudarlo con los dos 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));