Разве Code Contracts не может определить очевидную связь между Nullable <T>.HasValue и null? - PullRequest
11 голосов
/ 27 июля 2011

Я экспериментирую с применением кодовых контрактов к моему коду и столкнулся с недоумением.Этот код не соответствует контракту, но, если я не очень умный, я ожидаю, что он сможет легко проанализировать, что 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

Ответы [ 3 ]

6 голосов
/ 27 июля 2011

Я понял суть этого поведения, и это не ошибка Code Contract.

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

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

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

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

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

1 голос
/ 27 июля 2011

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

0 голосов
/ 27 июля 2011

Это не видит ваш, если бросить чек в рамках своих контрактов.Попробуйте вместо этого:

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

Contract.EndContractBlock();

http://msdn.microsoft.com/en-us/library/system.diagnostics.contracts.contract.endcontractblock.aspx

...