CODEWITHSUNDEEP
c#.netcode-contracts
Daniel Hilgarth
Daniel Hilgarth

Reputation: 174329

Unproven Ensure that references another property in combination with an interface

Assume the following code:

[ContractClass(typeof(ICC4Contract))]
public interface ICC4
{
    bool IsFooSet { get; }
    string Foo { get; }
}

public class CC4 : ICC4
{
    private string _foo;

    public bool IsFooSet { get { return Foo != null; } }

    public string Foo { get { return _foo; } }
}

[ContractClassFor(typeof(ICC4))]
public abstract class ICC4Contract : ICC4
{
    public bool IsFooSet
    {
        get
        {
            Contract.Ensures((Contract.Result<bool>() && Foo != null)
                             || !Contract.Result<bool>());
            return false;
        }
    }

    public string Foo
    {
        get
        {
            Contract.Ensures((Contract.Result<string>() != null && IsFooSet)
                             || !IsFooSet);
            return null;
        }
    }
}

The contracts try to say:

  1. IsFooSet will return true if Foo is not null.
  2. Foo doesn't return null if IsFooSet returns true.

This almost works.
However, I get an "ensures unproven" on return _foo;, because the checker doesn't realize that Foo will always equal _foo.

Changing Foo to an automatic property with a private setter removes that warning, but I don't want to do that (I don't like automatic properties with private setters).

What do I have to change in the above code to make the warning go away while preserving the _foo field?

The following doesn't work:

  1. Changing IsFooSet to use _foo instead of Foo. It will result in an additional "ensures unproven" on IsFooSet.
  2. Adding an invariant Foo == _foo. This will result in an "invariant unproven" on the implicit, default constructor. Furthermore, on a real code-base the processing time of the static checker will be magnitudes higher.
  3. Adding Contract.Ensures(Contract.Result<string>() == _foo); to the getter of Foo as per this answer doesn't change anything.

Upvotes: 9

Views: 199

Answers (1)

Eli Arbel
Eli Arbel

Reputation: 22739

You can use short-circuiting to simplify the condition, and that works for some reason:

[ContractClassFor(typeof(ICC4))]
public abstract class ICC4Contract : ICC4
{
    public bool IsFooSet
    {
        get
        {
            Contract.Ensures(!Contract.Result<bool>() || Foo != null);
            return false;
        }
    }

    public string Foo
    {
        get
        {
            Contract.Ensures(!IsFooSet || Contract.Result<string>() != null);
            return null;
        }
    }
}

Upvotes: 2

Related Questions