Comments 54
Ну и что делать с этим?
P.S. @«Береженого — бог бережет! — сказала монашка, надевая презерватив на свечку»
(в каждой шутке есть доля шутки)
P.S. Автор высказывания — Андрей Кнышев, а вовсе не Задорнов.
В контракте нельзя рассчитывать на какие то вычисления. Если нужно, чтобы вычисления гарантированно производились всегда, то нужно выносить их отдельно от контракта.
Кроме того, в предикатах контрактов не должно быть побочных эффектов.
Если вычисления VERIFY() нужны только для проверки и больше ничего и не имеют побочных эффектов, то можно внести их в контракт.
Весьма неуклюжий синтаксис с использованием макросов.
Какой вариант синтаксиса является более неуклюжим?
ASSERT(z >= 0);или
[[ assert: z >= 0 ]];Конкретно в случае с assert и, если говорить только о внешнем виде, то — дело вкуса. Мне лично [[assert: z >= 0]] больше нравится.
Если появляется ещё и предусловие, то вариант из стандарта уже становится чуть нагляднее, а если появляется ещё и постусловие и несколько точек выхода из функции, то разница становится очевидной. Кроме того, макросы нельзя сделать частью интерфейса. Нельзя их поместить в заголовочный файл отдельно от реализации.
Если они вам не нравятся, можете их не использовать. Не вижу чем они портят язык.
Синтаксис, кстати, не то чтобы новый: это продолжение синтаксиса атрибутов, поэтому поломаться ничего не должно. А чтобы не замедлять компиляцию, можно выставить соответствующий build-level.
Кстати, эти самые атрибуты как-то тихо оказались в стандарте. В отличие от других новых фич C++ я что-то совсем не видел их обсуждения, бурления го, статей здесь же. Как так? Ведь казалось бы революционное изменение, позволяющее добавлять любую метаинформацию компилятору. Где статьи по написанию плагина со своим атрибутам к любимому компилятору? Статьи про внутреннее устройство атрибутов, про их возможности, историю возникновения, сравнения с макросами, шаблонами и D? Метапрограммирование на атрибутах? Где, наконец, статьи про вылавливания неуловимых багов, суть которых в новом атрибуте, ломающем давно написанный код и т.д. и т.п.?
чтобы правильная программа с атрибутами обладала той же семантикой, что и без них.
Если их использовать для кодогенерации (основной кейс, как мне кажется), то, например, программа может просто не компилироваться без них (ибо нет того, что они нагенерировали). Раз не компилируется, то сравнивать семантику не с чем, а значит можно сказать, что любая семантика, появляющаяся от атрибутов, корректная.
Ну то есть получается так — программа без атрибутов правильная, если добавите еще один файл с исходниками, содержащий то, что генерируют атрибуты.
Если их использовать для кодогенерации (основной кейс, как мне кажется), то, например, программа может просто не компилироваться без них (ибо нет того, что они нагенерировали).Нет, не может. В стандарте есть специальный пункт, что программа должна корректно компилироваться, встречая неизвестные компилятору атрибуты.
Когда говорят что-то, на что потом отвечают "Не вижу чем портят", обычно подразумевается, что автор-то может и не использовать, но точно будет читать код, где это будет, его компилятор точно будет компилировать код, где это будет и ему точно придется отлаживать код, где это будет. Так что "не использовать" никак не получается. И это отсутствие выбора удручает. Вот что имеют ввиду, когда говорят про "гвозди".
По теме: как предполагается проверять постусловие, если оно будет разным в зависимости от точки выхода?
Точка выхода — это имплементация. Если в разных путях есть более строгие контракты — можно добавить их [[ assert ]]'ами прямо перед выходом для проверки.
еще правильнее — разбить на разные функции, каждая со своим более узким контрактом и на входные и на выходные условия.
Все же самым наглядным было бы использование специальных типов, когда неправильный код просто не скомпилируется
if (a <= 0) {
//Do smth
} else {
//Don't do
}
Если я правильно понял ваш вопрос, то ответ — нет. Контракты не предназначены для ветвления. Только проверки. Причём функция должна работать также, как если бы контрактов вовсе не было.
По поводу
только для заданных до компиляции значений
Если функция, не constexpr, то она может ссылаться на не-constexpr локальные переменные из своей области видимости (есть нюанс с приватными и защищёнными полями класса).
Например:
int a = 1;
int foo(int n) [[ expects: a <= n ]];Функция не-constexpr — может ссылаться на не-constexpr переменную.
Я дважды неправильно высказался, я имел ввиду проверку передаваемых в аргументы данных и динамическую проверку т.е., софтина работает в cmd, ей вводятся данные и она выполняет проверку
Кажется понял о чём вы спрашиваете.
Если неправильные аргументы являются частью нормального потока выполнения программы, то контракты не подходят для проверки.
Нужно либо изменить архитектуру, либо отказаться от контрактов.
Т.е. когда в функцию пришёл аргумент, нарушающий контракт, то программа должна тут же завершиться.
Поэтому, при использовании контрактов, вызывающая сторона должна провести всю необходимую валидацию. А контракты просто проверяют корректность валидации.
использование логики Хоара это, во-первых, способ формального доказательства корректности программы в тех случаях, когда ошибки могут привести к катастрофе или гибели людей
А если нет угрозы катастрофы или гибели людей, то контракты не дают способ доказательства корректности программ?!
Если не угрозы катастрофы или гибели людей, то вам видимо и правда нужно доказательство корректности, а не для галочки. В таком случае стоит посмотреть в сторону более развитых систем типов и формальных методов доказательства корректности программ.
Нет. Если надо перед кем-то отчитаться о том, что сделали надёжно — используешь контракты. Если надо сделать надёжно — то используешь средства формальной верификации.
Жаль, что установку хандлера отдали на усмотрение компилятора…
Ожидал что либо сделают что-то вроде std::contract_violation_exception, которое бы вылетало в случае нарушения контракта в дебаге (а ::what() уже оставить деталям реализации), либо хотя бы std::set_contract_handler() (no-op в релизе с правом выкинуть функцию, ясное дело).
А так придётся делать что-то вроде
set_property(TARGET program PROPERTY CXX_CONTRACT_HANDLER "mynamespace::contract_handler")в CMake'е. И ещё получим варнинг от анализатора о неиспользуемой функции, прелестно.
Ещё не совсем понял один момент: чтобы проверять мои вызовы к либе на валидность, мне придётся её тоже собрать в debug? Звучит как-то не очень.
1. Логика Хоара позволяет доказывать не корректность алгоритма, а корректность программы. Это важно. Например, существует не один алгоритм сортировки массивов, пред- и постусловия у каждой конкретной реализации будут совпадать, только вот инварианты циклов и условия корректности будут существенно отличаться (как следствие, их доказательство).
2. Возможность проводить анализ частичной корректности программы (то есть соответствие её спецификации — «контрактам» в описываемой терминологии) существует достаточно давно: достаточно вспомнить проект VCC. Есть даже плагин для MS Visual Studio.
3. Совершенно неясен вопрос с семантикой. Например, как моделируется память?
[[ expects: n == 5 ]]
[[ ensures n: n == 7 ]]
{
int n;
int *p = &n;
*p = 6;
}
В данном примере в контрактах побочных эффектов нет. Что будет в результате обработки данного кода?
4. Без инвариантов циклов всё это будет более-менее работать только в безцикловых программах (фрагментах программ). Причём автоматически породить инвариант цикла невозможно (в общем случае). И если пред- и постусловие программист в общем-то, думаю, в состоянии написать (или довести до ума в процессе отладки), то вот с инвариантами циклов не всё так просто. Причём чем выше уровень вложенности цикла, тем задача становится сложнее.
5. Ещё про семантику: как реально компилятор будет проверять соблюдение контрактов? Нужна семантика, чтобы порождать условия корректности, а потом их доказывать. С автоматическим доказательством в общем виде тоже всё плохо. В уже упомянутом VCC идёт связка с Z3 (SMT-решатель), но и тот не бог.
В целом начинание хорошее и полезное, хотя очевидно, что программисты к этому не готовы. Но в любом деле в начале всегда трудности. Спасибо за статью.
3 Совершенно неясен вопрос с семантикой
Такой пример не скомпилируется.
Если n определён в аргументах функции, то нельзя его переопределить.
Видимо вы имели ввиду вот такой пример
int foo(int n)
[[ expects: n == 5 ]]
[[ ensures n: n == 7 ]]
{
int *p = &n;
*p = 7;
return n;
}Нет никаких проблем. n в ensures будет идентификатором возвращаемого значения.
Хотя, конечно, так лучше не делать т.к. страдает читаемость кода
5 Ещё про семантику: как реально компилятор будет проверять соблюдение контрактов? Нужна семантика, чтобы порождать условия корректности, а потом их доказывать.
Я думаю компиляторы не будут заниматься формальным доказательством корректности программы по контрактам. Такие инструменты, наверное, можно будет сделать. Но это не задача компилятора. Задача компилятора просто проверить соблюдение контракта для каждой отдельно взятой функции и что-то сделать, в зависимости от настроек сборки. Например, вызывать std::terminate или violation_handler.
Задача компилятора просто проверить соблюдение контракта для каждой отдельно взятой функции
Так вот что это значит — «проверить соблюдение контракта»? Вы имеете ввиду для каждого конкретного вызова с конкретными значениями параметров? Ну тогда тут логика Хоара вообще не при чём.
хочу понять, как компилятор определит, что контракт не выполнен
При проверке постусловия не анализируется что происходит в теле функции. Просто проверяется предикат с теми значениями, которые получились при выходе из функции.
Ну тогда тут логика Хоара вообще не при чём
Про логику Хоара я упомянул чтобы было понятно откуда вообще контракты взялись и заинтересовавшиеся смогли изучить вопрос более глубоко.
Контракты предполагают несколько непривычный стиль написания программы. Поэтому я счёл разумным более детально описать мотивацию.
Стандарт не накладывает на компиляторы обязанность проверять корректность всей программы по контрактам. И программист может не описывать контракты для вообще всех функций в программе. Это допустимо. Но если всё же все контракты описаны, то проверить программу по логике Хоара возможно. Но не с помощью компилятора.
При проверке постусловия не анализируется что происходит в теле функции. Просто проверяется предикат с теми значениями, которые получились при выходе из функции.
Так в итоге, для примера выше — компилятор поймёт, что n не 7, а 6 при выходе из функции?
Стандарт не накладывает на компиляторы обязанность проверять корректность всей программы по контрактам. И программист может не описывать контракты для вообще всех функций в программе. Это допустимо. Но если всё же все контракты описаны, то проверить программу по логике Хоара возможно. Но не с помощью компилятора.
И в чём тогда польза? Не вижу тогда принципиального отличия от банального перебора различных значений параметров функции и возвращаемых значений.
Так в итоге, для примера выше — компилятор поймёт, что n не 7, а 6 при выходе из функции?
Да, конечно.
И в чём тогда польза?
вот:
какую пользу дают контракты:
- Улучшают читаемость кода за счёт явного документирования.
- Повышают надёжность кода, дополняя собой тестирование.
- Позволяют компиляторам использовать низкоуровневые оптимизации и генерировать более быстрый код.
Проверка корректности программы целиком возможно появится в статических анализаторах. Если каждая функция снабжена контрактом, то такая задача может быть решаемой.
пример:
[[какие то флаги]]
template<typename T, шаблоно-магия>
T foo(T a, T b, std::function<bool(const T &)> comp)
[[какие то флаги]]
[[какие то флаги]]
{ ...какая то магия...
return comp(a, b);
}
[[какой то флаг]]
auto res = foo<TA, TB, TZ <TA::bo, TZ::a>>(arg1, arg2, [](const TA &a){ return a.isValid();});Как говориться, не надо — не пользуйся, но это не отменяет того факта, что породиться код переполненный лямбдами, все возможными мета-обьектами на шаблонной магии. В перемешку с опционалами и флагами на каждом чихе и пуке.
Пробуем контрактное программирование С++20 уже сейчас