Кодовые контракты не могут обнаружить очевидную связь между Nullable <T>.HasValue и null?

Я экспериментирую с применением кодовых контрактов к моему коду, и я столкнулся с проблемой недоумения. Этот код не соответствует контракту, но если я не очень толстый, я бы ожидал, что он сможет легко проанализировать, что id должно иметь значение в точке возврата

if (id == null)
    throw new InvalidOperationException(string.Format("{0} '{1}' does not yet have an identity", typeof(T).Name, entity));

return id.Value;

Code Contracts error: requires unproven: HasValue

Ответы

Ответ 1

У меня есть нижняя часть этого поведения, и это не ошибка кода контракта.

Я открыл сгенерированную сборку в ILSpy, и это код, который создается:

public Guid Id
{
    get
    {
        Guid? guid = this.id;
        if (!guid.HasValue)
        {
            throw new InvalidOperationException();
        }
        guid = this.id;
        return guid.Value;
    }
}

Переменная экземпляра id копируется в локальную переменную, и эта локальная переменная reset возвращается к ее исходному значению после блока условий. Теперь стало очевидным, почему в кодовых контрактах показана ошибка, связанная с нарушением контракта, но она все же оставила меня в замешательстве, почему код был переписан в этой форме. Я сделал немного больше экспериментов и полностью выполнил кодовые контракты, и стало очевидно, что это стандартное поведение компилятора С#, но почему?

Секрет, похоже, объясняется незначительными деталями, которые я случайно пропустил из моего первоначального вопроса. Переменная экземпляра id объявляется как readonly, и это, по-видимому, отвечает за то, что компилятор добавляет временную переменную guid.

Я должен признать, что я все еще запутался, почему компилятор считает, что это нужно для обеспечения гарантии неизменности для id, но я продолжу копать...

Ответ 2

Вы можете попробовать скопировать поле в локальное значение и записать инструкции в терминах этого локального значения. Проверитель может быть консервативным в отношении полей, поскольку возможно, что вызов может изменить значение поля.