Требуется удовлетворить ограничения проверяемости для сгенерированного IL. Обратите внимание, что не поддается проверке не обязательно означает неверно . Он прекрасно работает без инструкции box, если его контекст безопасности позволяет запускать непроверяемый код. Проверка является консервативной и основана на фиксированном наборе правил (например, достижимость ). Чтобы упростить задачу, они решили не заботиться о наличии ограничений общего типа в алгоритме проверки.
Раздел 9.11: Ограничения общих параметров
...
Ограничения на универсальный параметр ограничивают только те типы, которые универсальный параметр
может быть создан с.
Проверка (см. Раздел III) требует, чтобы поле, свойство или метод
общий параметр , как известно, обеспечивает путем удовлетворения ограничения , не может
быть напрямую доступным / вызванным через универсальный параметр , если только он не заключен в первый квадрат
(см. Раздел III) или инструкция callvirt имеет префикс инструкции constrained. ...
Удаление инструкций box приведет к непроверяемому коду:
.method public hidebysig instance bool
F(!T r1,
!T r2) cil managed
{
ldarg.1
ldarg.2
ceq
ret
}
c:\Users\Mehrdad\Scratch>peverify sc.dll
Microsoft (R) .NET Framework PE Verifier. Version 4.0.30319.1
Copyright (c) Microsoft Corporation. All rights reserved.
[IL]: Error: [c:\Users\Mehrdad\Scratch\sc.dll : A`1[T]::F][offset 0x00000002][fo
und (unboxed) 'T'] Non-compatible types on the stack.
1 Error(s) Verifying sc.dll
ОБНОВЛЕНИЕ (Ответ на комментарий): Как я уже упоминал выше, проверяемость не эквивалентна правильности (здесь я говорю о «правильности» с точки зрения безопасности типов). Проверяемые программы являются строгим подмножеством правильных программ (то есть все проверяемые программы наглядно верны, но есть правильные программы, которые не поддаются проверке). Таким образом, проверяемость является более сильным свойством, чем правильность. Поскольку C # является языком, полным по Тьюрингу, Теорема Райса гласит, что доказательство правильности программ в общем случае неразрешимо.
Давайте вернемся к моей достижимости аналогии, поскольку это легче объяснить. Предположим, вы разрабатывали C #. Одна вещь, о которой подумал, - это когда выдавать предупреждение о недоступном коде и вообще удалять этот кусок кода в оптимизаторе, но как вы собираетесь обнаруживать весь недоступный код? Опять же, теорема Райс говорит, что вы не можете сделать это для всех программ. Например:
void Method() {
while (true) {
}
DoSomething(); // unreachable code
}
Это то, о чем на самом деле предупреждает компилятор C #. Но это не предупреждает о:
bool Condition() {
return true;
}
void Method() {
while (Condition()) {
}
DoSomething(); // no longer considered unreachable by the C# compiler
}
Человек может доказать, что поток управления никогда не достигает этой линии в последнем случае. Можно утверждать, что компилятор может статически доказать, что DoSomething также недоступен в этом случае, но это не так. Зачем? Дело в том, что вы не можете сделать это для всех программ, поэтому вы должны нарисовать линию в в некоторой точке . На этом этапе вы должны определить свойство decidable и назвать его «достижимость». Например, для достижения, C # придерживается константных выражений и вообще не будет смотреть на содержимое функций. Простота анализа и согласованность дизайна являются важными целями при принятии решения о том, где провести черту.
Возвращаясь к нашей концепции проверяемости, это аналогичная проблема. Проверяемость, в отличие от правильности, является решаемым свойством. Как разработчик среды выполнения, вы должны решить, как определить проверяемость, исходя из соображений производительности, простоты реализации, простоты спецификации, согласованности, облегчая компилятору уверенную генерацию проверяемого кода. Как и большинство дизайнерских решений, в нем много компромиссов. В конечном счете, разработчики CLI решили, что они предпочитают вообще не рассматривать общие ограничения при проверке на проверяемость.