Contratos de código: ¿Por qué algunos invariantes no se consideran fuera de la clase?

Question

consideran este tipo inmutable:

public class Settings 
{ 
    public string Path { get; private set; } 

    [ContractInvariantMethod] 
    private void ObjectInvariants() 
    { 
     Contract.Invariant(Path != null); 
    } 

    public Settings(string path) 
    { 
     Contract.Requires(path != null); 
     Path = path; 
    } 
} 

Dos cosas a notar aquí:

• hay un contrato invariante que asegura la propiedad Path nunca puede ser null
• El constructor comprueba el valor path argumento para respetar el contrato anterior invariante

En este punto, una instancia Setting nunca puede tener una propiedad nullPath.

Ahora, mira a este tipo:

public class Program 
{ 
    private readonly string _path; 

    [ContractInvariantMethod] 
    private void ObjectInvariants() 
    { 
     Contract.Invariant(_path != null); 
    } 

    public Program(Settings settings) 
    { 
     Contract.Requires(settings != null); 
     _path = settings.Path; 
    } // <------ "CodeContracts: invariant unproven: _path != null" 
} 

Básicamente, tiene su propio contrato invariante (en _path campo) que no puede ser satisfecha durante la comprobación estática (véase comentario anterior). Eso suena un poco raro para mí, ya que es fácil de demostrar que:

• settings es inmutable
• settings.Path no puede ser nulo (debido a la configuración tiene el contrato correspondiente invariante)
• por lo asignando settings.Path a _path, _path no puede ser nulo

¿Echaba de menos algo aquí?

Answer 1

Después de comprobar la code contracts forum, encontré this similar question con la siguiente respuesta por parte de uno de los desarrolladores:

Creo que el comportamiento que está experimentando es causada por alguna inferencia intermétodo que está pasando. El verificador estático primero analiza los constructores, luego las propiedades y luego los métodos. Al analizar el constructor de Sample, no sabe que msgContainer.Something! = Null, por lo que emite la advertencia. Una forma de resolverlo es agregar una suposición msgContainer.Something! = Null en el constructor, o mejor agregar la condición posterior! = Null a Something.

En otras palabras, las opciones son:

1. hacer que la propiedad Settings.Path explícita en lugar de automático, y especifique el invariante en el campo respaldo en su lugar. Para satisfacer su invariante, deberá agregar una condición previa al acceso del conjunto de la propiedad: Contract.Requires(value != null).

   Opcionalmente, puede agregar una condición posterior al descriptor de acceso get con Contract.Ensures(Contract.Result<string>() != null), pero el verificador estático no se quejará de ninguna manera.

2. Agregue Contract.Assume(settings.Path != null) al constructor de la clase Program.

Answer 2

Los invariantes no funcionan en miembros privados, no se puede saber por qué es así, espero que esto ayude.