¿Es esto un error en el comprobador de contrato estático?

Question

Si escribo esto:

public sealed class Foo 
{ 
    private int count; 
    private object owner; 
    private void Bar() 
    { 
     Contract.Requires(count > 0); 
     Contract.Ensures(owner == null || count > 0); 

     if (count == 1) 
      owner = null; 
     --count; 
    } 
} 

El corrector contrato estática puede probar todas las afirmaciones.

Pero si escribo esto en su lugar:

public sealed class Foo 
{ 
    private int count; 
    private object owner; 
    private void Bar() 
    { 
     Contract.Requires(count > 0); 
     Contract.Ensures(owner == null || count > 0); 

     --count; 
     if (count == 0) 
      owner = null; 
    } 
} 

Se afirma que la condición posterior owner == null || count > 0 no está comprobada.

creo que puedo probar la segunda forma no viola esta condición posterior:

// { count > 0 } it's required 
--count; 
// { count == 0 || count > 0 } if it was 1, it's now zero, otherwise it's still greater than zero 
if (count == 0) 
{ 
    // { count == 0 } the if condition is true 
    owner = null; 
    // { count == 0 && owner == null } assignment works 
} 
// { count == 0 && owner == null || count != 0 && count > 0 } either the if was entered or not 
// { owner == null || count > 0 } we can assume a weaker postcondition 

algo mal con mi prueba?

he añadido las afirmaciones en mi prueba como Contract.Assert llamadas al código, y llegaron a la conclusión de que si añado simplemente éste, se las arregla para probar la condición posterior:

--count; 
Contract.Assert(count == 0 || count > 0) 
if (count == 0) 
    owner = null; 

Pero, si ahora cambia esa misma afirmación de una manera "más natural", se produce un error:

--count; 
Contract.Assert(count >= 0) 
if (count == 0) 
    owner = null; 

sería de esperar que estas dos afirmaciones son equivalentes, pero el de electricidad estática los trata de manera diferente.

(estoy usando la beta 2 de VS10 por cierto)

Answer 1

No esperaría que esta prueba tan compleja esté en pleno funcionamiento aún, ya que es solo una versión beta después de todo. Creo que es un error o al menos un punto que vale la pena plantear a los desarrolladores, porque esto es algo muy simple para la comprobación estática de forma automática.

De todos modos, por el aspecto de las cosas, el marcador asegura está ahí para decir si el verificador de contrato estático es capaz de garantizar la condición o no. Esto no implica que la condición no sea válida, solo significa que no puede encontrar una prueba.

Estaría mucho más preocupado por los casos en los que se dice que algo está asegurado y que no es válido. ¡Eso contaría como un error!

Answer 2

Advertencia: Yo sé absolutamente nada acerca de los detalles del sistema de contratos .net.

Sin embargo, puedo decirles esto: es literalmente imposible (véase el problema de detención) para producir un comprobador completo para aserciones tan ricas como la que parece que este sistema admite.

Entonces, ¿esto es un error? No.

Por otro lado, parece plausible sugerir que este podría ser un caso común que los implementadores del probador podrían querer agregar a su sistema.