OberonCore
https://forum.oberoncore.ru/

Опасный ASSERT
https://forum.oberoncore.ru/viewtopic.php?f=86&t=6001
Страница 1 из 1

Автор:  Comdiv [ Вторник, 31 Январь, 2017 00:01 ]
Заголовок сообщения:  Опасный ASSERT

Для контроля корректности кода рекомендуется почаще использовать assert. Но есть и риск появление ошибок в самих assert. Чем больше assert'ов, тем больше в них ошибок, в том числе и не выявленных на тестировании. Это может быть проблемой для критических областей, если assert послужит причиной ошибочной аварийной остановки, которой бы не было без него - инструмента борьбы с ошибками.

Что-то можно было бы предпринять, например, игнорирование assert, внутри которого произошло обращение по нулевому указателю или выход за границы массива, но, в целом, проблема остаётся для таких assert, в которых нет очевидной ошибки, но условие составлено неправильно.

Какие есть соображения по этому поводу? Часто ли вы сталкиваетесь с ошибочными assert'ами? Проводил ли кто сопоставление пользы и вреда assert'ов?

Автор:  Илья Ермаков [ Вторник, 31 Январь, 2017 00:45 ]
Заголовок сообщения:  Re: Опасный ASSERT

Comdiv писал(а):
Это может быть проблемой для критических областей, если assert послужит причиной ошибочной аварийной остановки, которой бы не было без него - инструмента борьбы с ошибками.


Вот это ключевая фраза.
Если речь о некритических приложениях/компонентах, то не вижу проблемы:
- ASSERT призван отловить уже где-то ранее по ходу выполнения произошедшую ошибку, которая иначе бы проскочила "тихой сапой" дальше или вообще до конца (до некорректного результата).
- ошибки, которые проявляются в той строке, где и допущены - они могут быть где угодно, хоть в ASSERT, хоть не в ASSERT. С таким же успехом можно просто обсудить тему "если я увеличиваю объём кода на 5%, сколько ошибок я внесу?", типа того.

В ответственных приложениях, конечно, отказоустойчивость должна обеспечиваться обработкой исключений на верхнем уровне рабочего цикла приложения - и какой-то стратегией восстановления. Как в Erlang (и его soft-realtime нише): дохнет отдельная задача, есть обработчик этого сдыхания. И т.п.

Автор:  Comdiv [ Вторник, 31 Январь, 2017 00:59 ]
Заголовок сообщения:  Re: Опасный ASSERT

Илья Ермаков писал(а):
- ошибки, которые проявляются в той строке, где и допущены - они могут быть где угодно, хоть в ASSERT, хоть не в ASSERT. С таким же успехом можно просто обсудить тему "если я увеличиваю объём кода на 5%, сколько ошибок я внесу?", типа того.

5 % кода могут быть разными. Могут быть критически важными, а могут быть вспомогательными - как в ASSERT. Вот и хочется понять, как извлекая пользу из вспомогательного кода, минимизировать исходящие от него риски для основного кода.

Вопрос, конечно, можно поставить и шире, кроме ASSERT'ов есть и другой, менее специализированный вспомогательный код. Можно ли ещё что-то придумать, кроме обработки исключений на верхнем уровне?

Автор:  prospero78 [ Вторник, 31 Январь, 2017 08:16 ]
Заголовок сообщения:  Re: Опасный ASSERT

Вовсе необязательно использовать ASSERT. Прекрасную репутацию заслужил Debug.Out. Тоже самое, но без остановки кода. По хорошему, на все возможные ситуации должен быть предусмотрен обработчик. А если ситуация, которая по замыслу невозможна, но всё же случилась -- тут ассертов не напасёшься. Поэтому инженеры и не рассматривают такие случаи.

Автор:  Rifat [ Вторник, 31 Январь, 2017 09:47 ]
Заголовок сообщения:  Re: Опасный ASSERT

В книге "Verification of sequential and concurrent programs" есть раздел 1.5 Assertional Methods in Practice где написано:
Цитата:
Checking whether an implementation (a program) satisfies a contract is
done either by formal verification using proof rules (as outlined above) or —in
a limited way— at runtime. The second approach requires that the assertions
in the contracts are Boolean expressions. Then during each particular run of
the implementation it is checked automatically whether along this run all
assertions of the contract are satisfied. If an assertion is encountered that is
not satisfied, a failure or exception is raised.

Перевод:
Цитата:
Проверка того, удовлетворяет ли реализация (программы) контракту, проводится или путем формальной верификации, используя правила доказательств (как описано выше) или ограниченная проверка может выполняться во время выполнения программы. Второй подход требует чтобы утверждения контрактов были логическими выражениями. Затем во время каждого запуска программы все утверждения вдоль пути выполнения автоматически проверяются на то, что они выполняются. Если обнаруживается, что утверждение не выполняется, то возникает ошибка или исключение.


Таким образом, можно вообще не использовать assert в runtime, а использовать первый подход: формальная верификация.

Автор:  prospero78 [ Вторник, 31 Январь, 2017 10:11 ]
Заголовок сообщения:  Re: Опасный ASSERT

Рифат -- последовательный сторонник программирования под доказательство))
Вот ждал, что обязательно здесь подпишется!))
Проблему верификации уже обсуждали. Кто проверит верификатор? Кто даст гарантию, что верификатор проверяет семантическую правильность алгоритма , а не формальную?

Автор:  Rifat [ Вторник, 31 Январь, 2017 10:35 ]
Заголовок сообщения:  Re: Опасный ASSERT

Верификатор сам себя проверит. Также как есть компиляторы, которые сами себя компилируют bootstrapping-ом, также можно написать и верификатор, который проверит свой собственный же код, но пока насколько я знаю такого еще нет.

Автор:  Comdiv [ Вторник, 31 Январь, 2017 12:45 ]
Заголовок сообщения:  Re: Опасный ASSERT

Да, формальное доказательство - это идеал, к которому надо стремиться. И, пожалуй, для критических областей это должно стать нормой. Но попробовав на практике пару существующих решений, должен сказать, что это накладно, а без дополнительного обучения вообще не даётся. Рассчитывать на массовое применение не приходится, поэтому нужны компромиссные решения - не полноценные, но легко пишущиеся.

Автор:  Rifat [ Вторник, 31 Январь, 2017 12:55 ]
Заголовок сообщения:  Re: Опасный ASSERT

Согласен с "Но попробовав на практике пару существующих решений, должен сказать, что это накладно, а без дополнительного обучения вообще не даётся. "
Первично - это знание ручной верификации, если знать и владеть этим методом, то можно и утилиты какие-нибудь использовать. А без знаний, утилиты будут бесполезны.

Автор:  Comdiv [ Вторник, 31 Январь, 2017 14:39 ]
Заголовок сообщения:  Re: Опасный ASSERT

Позвольте уточнить - без дополнительного обучения использованию утилиты.
Вот простой пример использования ANSI C Specification Language.
Код:
/*@
  ensures \result ==> (*p == m1 * m2);
  ensures \result == (0 <= m1 * m2 <= UINT_MAX);
*/
bool mult(unsigned *p, unsigned m1, unsigned m2) {
   bool correct = (0 == m2) || ((UINT_MAX / m2) >= m1);
   if (correct) {
      *p = m1 * m2;
   }
   return correct;
}

Этот элементарный пример ставит в ступор систему доказательства. Я знаю, как это доказать вручную, но утилите это не поможет. Попробовав разобраться с этим через документацию, я не получил результата. Подумал, что в Ada/SPARK должно быть проще, но там получил то же самое. Нашёл информацию, что есть специальная библиотека, позволяющая доказывать такие вещи, но в свободной поставке я её не нашёл.

Ручного доказательства категорически недостаточно. Перепутает человек названия переменных и не заметит, или совершит любую другую ошибку внимательности. Ручное доказательство будет верным, а программа - нет.

Автор:  Rifat [ Вторник, 31 Январь, 2017 15:01 ]
Заголовок сообщения:  Re: Опасный ASSERT

В примере, который вы привели, не указано предусловие, а только постусловие. Предусловие обычно обозначается словом require. Возможно, что из-за этого доказательство не было успешным.

Автор:  Comdiv [ Вторник, 31 Январь, 2017 15:20 ]
Заголовок сообщения:  Re: Опасный ASSERT

Нет, не поэтому. Предусловия не всегда нужны, так как любые параметры допустимы. В данном случае это не так из-за того, что это Си и в функцию может быть передан неправильный указатель. В оригинале я указывал
Код:
requires \valid(p);
Но я посчитал эту часть слишком неважной для примера. В принципе, Frama-C не требует этого.

Страница 1 из 1 Часовой пояс: UTC + 3 часа
Powered by phpBB® Forum Software © phpBB Group
https://www.phpbb.com/