Комментарии 26
Я правильно понимаю, что контракт — это что-то вроде трех последовательных методов, работающих с одним набором данных, первый из которых выполняет проверки, второй — модифицирует данный, а третий — проверяет их допустимость?
Контракт — это развитие представления о верифицируемости кода для императивного программирования.
Так как для мейнстрим-языков (императивных, в основном) формальный анализ корректности представляется необозримо сложным (потому что в императивном языке модель потоков данных вторична, и потому ее крайне труждоемко отследить и упорядочить), сделана попытка ввести предположения, упрощающие этот анализ.
Для этого делается попытка привязать граф потоков данных к графу потоков управления — в ключевых точках последнего (вход в процедуру/выход в процедуру/некоторые другие ключевые точки) данные анализируются на предмет соответствия ожидаемым данным в этих точках.
Кроме того, контракт — это еще и самодокументирование кода.
Так как для мейнстрим-языков (императивных, в основном) формальный анализ корректности представляется необозримо сложным (потому что в императивном языке модель потоков данных вторична, и потому ее крайне труждоемко отследить и упорядочить), сделана попытка ввести предположения, упрощающие этот анализ.
Для этого делается попытка привязать граф потоков данных к графу потоков управления — в ключевых точках последнего (вход в процедуру/выход в процедуру/некоторые другие ключевые точки) данные анализируются на предмет соответствия ожидаемым данным в этих точках.
Кроме того, контракт — это еще и самодокументирование кода.
В данный момент (.net contracts) это реализовано при помощи инструментирования сборок, чтобы обеспечить как compile-time-, так и runtime-анализ, но ничего не мешает выполнять, например, только compile-time анализ.
Контракт — это набор некоторых условий, которые должны быть верны перед вызовом метода (подпрограммы) для предусловия и должны быть верны при выходе из метода (для постусловия).
Например, есть метод
double GetSqrt(double d)
{
…
}
Можно написать условие проверки d на неотрицательность, а можно написать контракт
Contract.Requires(d>=0);
И теперь всем понятно, что неотрицательное d — требование спецификации, кроме того в релиз-версии данная проверка не будет проводиться. Я пока не разобрался с наследованием, но, как я понимаю, при переопределении контракт должен сохраняться. Причем предусловие может ослабевать, а постусловие усиливаться.
Для постусловий тоже самое. При выходе из метода мы можем что-либо сказать нашим клиентам, по поводу возвращаемого результата ил состояния объекта.
public double Sum()
{
double res = 0;
...// какой-то код
Contract.Ensures(res > 0); // res > 0 и я гарантирую это, говорит нам метод с контрактом
return res;
}
то есть метод никак не сможет вернуть значение меньшее или равное единицы, поэтому если вам, в вашем методе требуется положительное double, вы можете смело и БЕЗ ПРОВЕРКИ использовать результат данного метода, ибо контракт.
Например, есть метод
double GetSqrt(double d)
{
…
}
Можно написать условие проверки d на неотрицательность, а можно написать контракт
Contract.Requires(d>=0);
И теперь всем понятно, что неотрицательное d — требование спецификации, кроме того в релиз-версии данная проверка не будет проводиться. Я пока не разобрался с наследованием, но, как я понимаю, при переопределении контракт должен сохраняться. Причем предусловие может ослабевать, а постусловие усиливаться.
Для постусловий тоже самое. При выходе из метода мы можем что-либо сказать нашим клиентам, по поводу возвращаемого результата ил состояния объекта.
public double Sum()
{
double res = 0;
...// какой-то код
Contract.Ensures(res > 0); // res > 0 и я гарантирую это, говорит нам метод с контрактом
return res;
}
то есть метод никак не сможет вернуть значение меньшее или равное единицы, поэтому если вам, в вашем методе требуется положительное double, вы можете смело и БЕЗ ПРОВЕРКИ использовать результат данного метода, ибо контракт.
спасибо за статью — недавно наткнулся на эту статью в msdn и отложил на прочтение на потом.
P.S. Подредактируйте предложение — «Предусловия и постусловия описывают свойства отдельных программ. но экземпляры класс обладают также глобальными свойствами.»
P.S. Подредактируйте предложение — «Предусловия и постусловия описывают свойства отдельных программ. но экземпляры класс обладают также глобальными свойствами.»
Вроде та же идея используется в формальных методах доказательства алгоритмов.
Было интересно почитать, спасибо.
Было интересно почитать, спасибо.
Да, знакомые вещи, старые идеи и это даже не середина 90ых, а гораздо раньше, смотрите работы
Дейкстры, например «Дисциплина программирования», все это от туда формальное доказательство правильности алгоритмов, слабейшее предусловие и прочие радости :)
Тут более интересно войдет ли это все когда нибудь в мейнстрим?
Дейкстры, например «Дисциплина программирования», все это от туда формальное доказательство правильности алгоритмов, слабейшее предусловие и прочие радости :)
Тут более интересно войдет ли это все когда нибудь в мейнстрим?
Хз, но надежда есть :).
Например, Midori — инициатива M$ по созданию формально верифицируемой ОС. Они так рьяно взялись за это дело, что даже перекупили себе в MS Research разработчика BitC (язык) и Coyotous (первый и единственный прототип формально верифицируемой ОС), «заставив» его прекратить разработку вышеупомянутых проектов.
Другое дело, что вряд ли это интересно большинству. Как вы себе представляете формально доказанный магазин на php? :)
Например, Midori — инициатива M$ по созданию формально верифицируемой ОС. Они так рьяно взялись за это дело, что даже перекупили себе в MS Research разработчика BitC (язык) и Coyotous (первый и единственный прототип формально верифицируемой ОС), «заставив» его прекратить разработку вышеупомянутых проектов.
Другое дело, что вряд ли это интересно большинству. Как вы себе представляете формально доказанный магазин на php? :)
о, а я инвариатны видел в языке D)) И кстати как понял, условия проверяются только в отлдаочной сборке, а в release отключаются, да?
НЛО прилетело и опубликовало эту надпись здесь
Как я понял наследованием и наличием инвариантов.
Ну и назначение немного другое: ассертами мы для себя проверяем какие-либо условия в любых точках. Здесь мы проверяем условие на входе или выходе и всем гарантируем (и требуем!) соблюдение контракта, что, в итоге, должно повысить качество кода, убрать лишние проверки, ускорить отладку.
Например, Вы сделали некий метод, в котором по контракту возвращается положительное число. При использовании Вашего метода, как входа своего
double d = MyMath.GetSqrt(yourClass.YourMethodWithPositiveReturnByContract())
Я НЕ БУДУ проверять, что Ваш метод возвращает положительное число, я верю контракту.
Если Вы сделаете проверку с помощью Assert — то Вы, может быть, убедите только себя в положительности результата, я верить не буду и включу проверку на неотрицательность.
Как-то так.
Ну и назначение немного другое: ассертами мы для себя проверяем какие-либо условия в любых точках. Здесь мы проверяем условие на входе или выходе и всем гарантируем (и требуем!) соблюдение контракта, что, в итоге, должно повысить качество кода, убрать лишние проверки, ускорить отладку.
Например, Вы сделали некий метод, в котором по контракту возвращается положительное число. При использовании Вашего метода, как входа своего
double d = MyMath.GetSqrt(yourClass.YourMethodWithPositiveReturnByContract())
Я НЕ БУДУ проверять, что Ваш метод возвращает положительное число, я верю контракту.
Если Вы сделаете проверку с помощью Assert — то Вы, может быть, убедите только себя в положительности результата, я верить не буду и включу проверку на неотрицательность.
Как-то так.
Та нет, все проще. :)
Контракты представляют собой более-менее дисциплинированное применение assert(). Однако же идея восходит к соответствию Карри-Говарда, которое как бы намекает нам, что
— между системами типов и логическими система есть соответствие
— программы являются доказательствами
Например, тип функции fact (факториал), что-то вроде
fact: forall x, x >= 0, exists y, y >= 0; x -> y
Ну а доказательством этого утверждения является программа.
Контракты представляют собой более-менее дисциплинированное применение assert(). Однако же идея восходит к соответствию Карри-Говарда, которое как бы намекает нам, что
— между системами типов и логическими система есть соответствие
— программы являются доказательствами
Например, тип функции fact (факториал), что-то вроде
fact: forall x, x >= 0, exists y, y >= 0; x -> y
Ну а доказательством этого утверждения является программа.
Если я правильно понял, то указанный подход изоморфен юнит-тестируемому результату проектирования + моковый фреймворк.
Фишка контрактов в изначальной интегрируемости?
Фишка контрактов в изначальной интегрируемости?
Здесь я пытался объяснить чем отличается использование Assert от контрактов на мой взгляд. Контракт после релиза ваших сборок доступен клиентам (в смысле не конечным пользователям, а тем кто будет использовать ваши сборки в своей работе, например ваш коллега), тесты и ассерты не всегда.
Инвариантов вообще никак не сделать без огромного дублирования кода, что есть зло. Таким образом, с помощью инвариантов легко поддерживать объект в согласованном состоянии.
Третий момент — наследование. Я пока не разбирался с наследованием контрактов в .Net, но в оригинале (у Мейера) контракты наследуются, чего опять же нет при использовании ассертов и тестов. Причем предусловие может ослабевать, а постусловие усиливаться при переходе к дочерним классам.
Инструменты — в том числе попытка проверки кода без его запуска.
Инвариантов вообще никак не сделать без огромного дублирования кода, что есть зло. Таким образом, с помощью инвариантов легко поддерживать объект в согласованном состоянии.
Третий момент — наследование. Я пока не разбирался с наследованием контрактов в .Net, но в оригинале (у Мейера) контракты наследуются, чего опять же нет при использовании ассертов и тестов. Причем предусловие может ослабевать, а постусловие усиливаться при переходе к дочерним классам.
Инструменты — в том числе попытка проверки кода без его запуска.
хм. ну да, понятно.
Юниттесты все же круче тем, что они отделены от кода, тогда как контракты должны быть с ним тесно связаны.
Но тема интерсная, спасибо.
Юниттесты все же круче тем, что они отделены от кода, тогда как контракты должны быть с ним тесно связаны.
Но тема интерсная, спасибо.
вы можете использовать контракт просто как документацию в релизах (также с Assert сейчас).
Есть возможность проверки с помощью ccrewrite.exe — примерно так-же, как NUnit (руками пока ничего не трогал, все в теории).
Вы можете отделить контракт от кода и получить чистый контракт — с помощью ccrefgen.exe
Ну и попытаться проверить контракт без запуска сборки на основе кода (статически) с помощью утилиты cccheck.exe.
В ближайшее время планирую изучить подробнее данные инструменты и сделать обзор.
Ну а насчет связки контракта и кода — наоборот это плюс, имхо. Ведь именно контракт показывает что вы ждете на входе и что будет на выходе. Тесты и ассерты для внутреннего потребления, контракты при взаимодействии сборок различных поставщиков.
Есть возможность проверки с помощью ccrewrite.exe — примерно так-же, как NUnit (руками пока ничего не трогал, все в теории).
Вы можете отделить контракт от кода и получить чистый контракт — с помощью ccrefgen.exe
Ну и попытаться проверить контракт без запуска сборки на основе кода (статически) с помощью утилиты cccheck.exe.
В ближайшее время планирую изучить подробнее данные инструменты и сделать обзор.
Ну а насчет связки контракта и кода — наоборот это плюс, имхо. Ведь именно контракт показывает что вы ждете на входе и что будет на выходе. Тесты и ассерты для внутреннего потребления, контракты при взаимодействии сборок различных поставщиков.
Контракт тоже можно отделить от кода. Например, использование аспектно-ориентированного программирования позволяет это сделать. Или вообще специализированные технологии описания контрактов типа UniTESK или Spec#.
А никто не задумывался, как это повлияет на производительность кода?
>второй гарантирует выброс исключения при нарушении контракта.
Неправда. Он гарантирует, что при вылете исключения будет соблюдено условие (например, не изменится переданное по ссылке значение).
Опять же, невнятно написано что компилируется в Release, а что нет.
Неправда. Он гарантирует, что при вылете исключения будет соблюдено условие (например, не изменится переданное по ссылке значение).
Опять же, невнятно написано что компилируется в Release, а что нет.
Спасибо, подправил.
Насчет компиляции.
В свойства проекта добавляется новая закладка Code Contracts, там мы и выбираем, будет проверка контракта рантайм или нет, если будет, то в каком виде (Assert или выброс исключения). Так в студии. На самом деле мы просто выбираем чем компилировать нашу сборку — обычным компилятором или с помощью ccrewrite.exe. Второй вариант включает проверки контрактов.
Насчет компиляции.
В свойства проекта добавляется новая закладка Code Contracts, там мы и выбираем, будет проверка контракта рантайм или нет, если будет, то в каком виде (Assert или выброс исключения). Так в студии. На самом деле мы просто выбираем чем компилировать нашу сборку — обычным компилятором или с помощью ccrewrite.exe. Второй вариант включает проверки контрактов.
The other form, Requires, makes that same statement, but further guarantees that if the condition is not met, an exception of type TException should be thrown. It is also unique in that it is always compiled, so use of this method entails a hard dependency on the tools. You should decide if you want that before using this method.
>В данном примере контракт будет нарушен. Также учтены усиления-ослабления условий.
>По Мейеру, наследник имеет право ослабить предусловие (большее количество вариантов принимать)
>и усилить постусловие — еще больше ограничить возвращаемое значение.
В наследниках нельзя ни усилить, ни ослабить контракт. См. их официальный pdf-ник (пункт 3).
>По Мейеру, наследник имеет право ослабить предусловие (большее количество вариантов принимать)
>и усилить постусловие — еще больше ограничить возвращаемое значение.
В наследниках нельзя ни усилить, ни ослабить контракт. См. их официальный pdf-ник (пункт 3).
Зарегистрируйтесь на Хабре, чтобы оставить комментарий
Программирование по контракту в .NET Framework 4