Контракты - статический анализ некорректно помечает Обеспечить условие - PullRequest
Новая
       23

Контракты - статический анализ некорректно помечает Обеспечить условие

2 голосов
/ 05 декабря 2010

Я потратил несколько часов на эту проблему ... вот мой код: 

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

По какой-то причине последняя строка (вызов Generate ()) помечается как "ensures unproven: Contract.ForAll<string>(Contract.Result<IEnumerable<string>>(), s => s != null)».Я не понимаю, как это может быть - Generate гарантирует, что он не возвратит нулевые элементы, и анализатор не жалуется на это.Что я делаю не так?

[Edit] Хмм ... вдруг я получаю предупреждение о функции Generate - тоже самое, гарантия не доказана.Могу поклясться, что этого не было раньше, но в любом случае - теперь проблема ушла.Как я могу убедить анализатор в том, что нет способа вернуть нулевые элементы?Или, в противном случае, где я ошибаюсь, и функция может вернуть нулевые элементы?

[Редактировать] Blech ... эта статья говорит "условия публикации (т. Е. Контракт).Ensure) не поддерживаются статической проверкой "(в итераторах) ... кто-нибудь может это подтвердить?

1 Ответ

1 голос
/ 07 декабря 2010

yield return в настоящее время не будет работать с Contract.Ensures из-за взаимодействия между компилятором и ccrewrite.

Лучшее, что вы можете сделать в данный момент - это написать приватный метод без контрактов, а затем Assume требуемые контракты в публичном методе: 

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