Различия между кодом контракта и спецификацией

Question

Я хочу реализовать DBC в C#. Я столкнулся с SpeC# и Кодексом контракта для этого.
В чем разница между SpeC# и Code Contract?

Answer 1

Это из часто задаваемых вопросов по контрактам на кодекс в Microsoft Research:

Контракты кода имеют какое-либо отношение к SpeC#?

Code Contracts является дополнительным продуктом проекта SpeC#. Основная задача SpeC# - понять значение инвариантов объектов при наличии наследования, обратных вызовов, псевдонимов и многопоточности. SpeC# является надмножеством C# v2.0 и использует переписчик исходного уровня для включения контрактов в код. Он использует генерацию условия проверки и средство проверки теорем для статической проверки кода SpeC#. Но разумное решение всех сложных вопросов, связанных с поддержанием объектных инвариантов, имеет свою цену: проверка становится нетривиальной. Вот почему SpeC# также нужна дисциплина владения, чтобы знать, какие объекты могут иметь псевдонимы или не могут иметь псевдонимы друг для друга.

Code Contracts - это результат изучения SpeC# того, что работает, а что нет. В отличие от SpeC#, кодовые контракты не зависят от языка и, следовательно, работают на всех языках.NET, от VB до C# и F#. Переписчик работает на MSIL и, следовательно, не зависит от конкретных компиляторов. Его механизм статического анализа использует абстрактную интерпретацию, которая намного быстрее и более предсказуема, чем проверка; Кроме того, абстрактная интерпретация выводит инварианты цикла и контракты методов, что помогает в принятии и простоте использования контрактов кода.

Таким образом, кажется, что Code Contracts будет более "поддерживаемым" инструментом в будущем.