У меня есть эта структура (упрощенная для краткости):
public struct Period
{
public Period(DateTime? start, DateTime? end) : this()
{
if (end.HasValue && start.HasValue && end.Value < start.Value)
{
throw new ArgumentOutOfRangeException("end", "...");
}
Contract.EndContractBlock();
this.start = start;
this.end = end;
}
private readonly DateTime? start;
private readonly DateTime? end;
public static Period operator +(Period p, TimeSpan t)
{
Contract.Assume(!p.start.HasValue || !p.end.HasValue || p.start.Value <= p.end.Value);
return new Period(
p.start.HasValue ? p.start.Value + t : (DateTime?) null,
p.end.HasValue ? p.end.Value + t : (DateTime?) null);
}
}
Но статическая проверка дает мне это предупреждение:
CodeContracts: требует недоказанных: end.HasValue && & start.HasValue && end.Value >= start.Value
Это требование, которое оно выводит из проверки пользовательских параметров, просто неверно. Я хочу разрешить нулевые значения для start или end, и требуется только start <= end, если оба они предусмотрены. Однако, если я сменил конструктор на это:
public Period(DateTime? start, DateTime? end) : this()
{
Contract.Requires(!start.HasValue || !end.HasValue || start.Value <= end.Value);
this.start = start;
this.end = end;
}
Я получаю это предупреждение, которое выглядит более правильным, но трудно понять, почему требования не могут быть доказаны:
CodeContracts: требует недоказанных:! start.HasValue ||! end.HasValue || start.Value <= end.Value
Я думал, что это может вызвать проблемы с ?:, но это предупреждение все еще существует, когда я меняю оператор на:
public static Period operator +(Period p, TimeSpan t)
{
var start = p.start.HasValue ? p.start.Value + t : (DateTime?) null;
var end = p.end.HasValue ? p.end.Value + t : (DateTime?) null;
Contract.Assume(!start.HasValue || !end.HasValue || start.Value <= end.Value);
return new Period(start, end);
}
И, конечно, если я изменю значение .Requires на .Assume, предупреждение полностью исчезнет, но это не приемлемое решение.
Таким образом, кажется, что статическая проверка в Code Contracts не может правильно инвертировать условие. Вместо того, чтобы просто инвертировать условие, обернув его !(…) или применив закон Де Моргана (как показано выше), он, похоже, инвертирует только последний компонент условия, Не удается ли статическому контролеру корректно интерпретировать сложные условные выражения при использовании выборочной проверки параметров?
Интересно, что я пробовал это, думая, что статический контролер просто разделит ! с фронта, но нет:
if (!(!start.HasValue || !end.HasValue || start.Value <= end.Value))
{
throw new ArgumentOutOfRangeException("end", "...");
}
Contract.EndContractBlock();
CodeContracts: требуется недоказанный:! (! (! start.HasValue ||! end.HasValue || start.Value <= end.Value))
В этом случае он просто завершил все условие с помощью !(…), даже если это не было.
Кроме того, если я изменяю значение nullable DateTime на простое значение, отличное от нуля, DateTime и переписываю такие контракты, он работает как ожидается без каких-либо предупреждений:
public struct Period
{
public Period(DateTime start, DateTime end) : this()
{
Contract.Requires(start <= end);
this.start = start;
this.end = end;
}
private readonly DateTime start;
private readonly DateTime end;
public static Period operator +(Period p, TimeSpan t)
{
Contract.Assume(p.start + t <= p.end + t); // or use temp variables
return new Period(p.start + t <= p.end + t);
}
}
Но просто использование Contract.Assume(p.start <= p.end) не будет работать.
CodeContracts: требует недоказанных: start <= end
