Contrats - analyse statique mal repérage Condition à remplir

Question

J'ai passé quelques heures sur cette question ... voici mon code:

public static IEnumerable<T> Generate<T>(this Func<T> generator) where T : class 
{ 
    Contract.Ensures(Contract.Result<IEnumerable<T>>() != null); 
    Contract.Ensures(Contract.ForAll<T>(Contract.Result<IEnumerable<T>>(), item => item != null)); 

    if (generator == null) 
    yield break; 

    T t; 
    while ((t = generator()) != null) 
    yield return t; 
} 


public static IEnumerable<string> ReadLines(this TextReader reader) 
{ 
    Contract.Requires(reader != null); 
    Contract.Ensures(Contract.Result<IEnumerable<string>>() != null); 
    Contract.Ensures(Contract.ForAll<string>(Contract.Result<IEnumerable<string>>(), s => s != null)); 

    return Generate(() => reader.ReadLine()); 
} 

Pour une raison quelconque, la dernière ligne (l'invocation de générer()) est marqué comme "ensures unproven: Contract.ForAll<string>(Contract.Result<IEnumerable<string>>(), s => s != null)". Je ne vois pas comment cela peut être le cas - Generate garantit qu'il ne renverra pas d'éléments NULL, et l'analyseur ne s'en plaindra pas. Qu'est-ce que je fais mal? [Edit] Hmm ... tout d'un coup, je reçois un avertissement sur la fonction Générer - même chose, l'assurance n'est pas prouvée. Je pourrais jurer que cela ne se passait pas avant, mais en tout cas - maintenant le problème a bougé. Comment puis-je persuader l'analyseur qu'il n'y a aucun moyen de renvoyer des éléments Null? Ou, alternativement, où ai-je tort et la fonction peut retourner des éléments null? [Modifier] Blech ... this article dit "les conditions de publication (c.-à-d. Contrat.Assurance) ne sont pas supportées par le vérificateur statique" (dans les itérateurs) ... quelqu'un peut-il confirmer cela?

Answer 1

yield return ne fonctionnera pas actuellement avec Contract.Ensures en raison d'interactions entre le compilateur et ccrewrite.

mieux que vous pouvez faire pour le moment est d'écrire une méthode privée sans contrat, puis Assume les contrats nécessaires à une méthode publique:

private static IEnumerable<T> RealGenerate<T>(this Func<T> generator) where T : class 
{ 

    if (generator == null) 
    yield break; 

    T t; 
    while ((t = generator()) != null) 
    yield return t; 
} 

public static IEnumerable<T> Generate<T>(this Func<T> generator) where T: class 
{ 
    Contract.Ensures(Contract.Result<IEnumerable<T>>() != null); 
    Contract.Ensures(Contract.ForAll(Contract.Result<IEnumerable<T>>(), item => item != null)); 

    var result = RealGenerate(generator); 
    Contract.Assume(result != null); 
    Contract.Assume(Contract.ForAll(result, item => item != null)); 
    return result; 
}