CODEWITHSUNDEEP
c#code-contracts
Mårten Wikström
Mårten Wikström

Reputation: 11344

How can I ensure that an iterator method will not yield any null items?

I'm wondering whether it is possible to ensure (using ) that an iterator method will never yield a null item.

This simplified method:

public static IEnumerable<object> CreateSomeObjects()
{
    Contract.Ensures(Contract.Result<IEnumerable<object>>() != null);
    Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<object>>(), _ => _ != null));

    for (int i = 0; i < 10; ++i)
    {
        yield return new object();
    }
}

Results in a compile time warning similar to this:

CodeContracts: MyClass.CreateSomeObjects()[0x9]: ensures unproven: Contract.ForAll(Contract.Result>(), _ => _ != null)

What can I do to prove it to the static checker?

Upvotes: 1

Views: 209

Answers (1)

Sebastian 506563
Sebastian 506563

Reputation: 7238

Only way you can put contracts on iterators is:

public class Graph
{
    public IEnumerable<Node> Nodes(Graph g)
    {
        Contract.Requires(g != null);
        Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<Nodei>>, node => node != null));
        foreach (var x in g.MethodForGettingNodes())
        yield return x;
    }
}

The contracts above make sure that callers don’t pass in a null parameter, and the method itself guarantees that all elements in the resulting collection are non-null.

Currently, the static checker does not reason about collections and thus will not be able to prove the postcondition above.

According to documentation they still do not fix it since 2009, I had problems with cc 2 years ago, and they still did not fix it and i think they wont.

Upvotes: 1

Related Questions