Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Code Contracts: Why are some invariants not considered outside the class?

Consider this immutable type:

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

Two things to notice here:

  • There is a contract invariant which ensures the Path property can never be null
  • The constructor checks the path argument value to respect the previous contract invariant

At this point, a Setting instance can never have a null Path property.

Now, look at this type:

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"
}

Basically, it has its own contract invariant (on _path field) that can't be satisfied during static checking (cf. comment above). That sounds a bit weird to me, since it's easy to prove it:

  • settings is immutable
  • settings.Path can't be null (because Settings has the corresponding contract invariant)
  • so by assigning settings.Path to _path, _path can't be null

Did I miss something here?

like image 454
Romain Verdier Avatar asked Jul 29 '10 14:07

Romain Verdier


People also ask

Can static methods have class invariants?

Static invariants must be established by the static initialization of a class, and must be preserved by all non-helper constructors and methods, i.e., by both static and instance methods.

What are the code contracts?

Code contracts provide a way to specify preconditions, postconditions, and object invariants in . NET Framework code. Preconditions are requirements that must be met when entering a method or property. Postconditions describe expectations at the time the method or property code exits.


1 Answers

After checking the code contracts forum, I found this similar question with the following answer from one of the developers:

I think the behavior you are experiencing is caused by some inter-method inference that is going on. The static checker first analyzes the constructors, then the properties and then the methods. When analyzing the constructor of Sample, it does not know that msgContainer.Something != null so it issues the warning. A way to solve it, is either by adding an assumption msgContainer.Something != null in the constuctor, or better to add the postcondition != null to Something.

So in other words, your options are:

  1. Make the Settings.Path property explicit instead of automatic, and specify the invariant on the backing field instead. In order to satisfy your invariant, you will need to add a precondition to the property's set accessor: Contract.Requires(value != null).

    You can optionally add a postcondition to the get accessor with Contract.Ensures(Contract.Result<string>() != null), but the static checker will not complain either way.

  2. Add Contract.Assume(settings.Path != null) to the constructor of the Program class.

like image 175
Rich Avatar answered Oct 25 '22 09:10

Rich