OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Пятница, 26 Май, 2017 10:24

Часовой пояс: UTC + 3 часа




Начать новую тему Ответить на тему  [ Сообщений: 12 ] 
Автор Сообщение
 Заголовок сообщения: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 00:01 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 379
Откуда: Киев
Для контроля корректности кода рекомендуется почаще использовать assert. Но есть и риск появление ошибок в самих assert. Чем больше assert'ов, тем больше в них ошибок, в том числе и не выявленных на тестировании. Это может быть проблемой для критических областей, если assert послужит причиной ошибочной аварийной остановки, которой бы не было без него - инструмента борьбы с ошибками.

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 00:45 
Модератор
Аватара пользователя

Зарегистрирован: Понедельник, 14 Ноябрь, 2005 18:39
Сообщения: 8695
Откуда: Россия, Орёл
Comdiv писал(а):
Это может быть проблемой для критических областей, если assert послужит причиной ошибочной аварийной остановки, которой бы не было без него - инструмента борьбы с ошибками.


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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 00:59 

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 08:16 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 931
Откуда: СССР v2.0 rc 1
Вовсе необязательно использовать ASSERT. Прекрасную репутацию заслужил Debug.Out. Тоже самое, но без остановки кода. По хорошему, на все возможные ситуации должен быть предусмотрен обработчик. А если ситуация, которая по замыслу невозможна, но всё же случилась -- тут ассертов не напасёшься. Поэтому инженеры и не рассматривают такие случаи.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 09:47 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 528
Откуда: Казань
В книге "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, а использовать первый подход: формальная верификация.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 10:11 
Аватара пользователя

Зарегистрирован: Воскресенье, 12 Апрель, 2015 18:12
Сообщения: 931
Откуда: СССР v2.0 rc 1
Рифат -- последовательный сторонник программирования под доказательство))
Вот ждал, что обязательно здесь подпишется!))
Проблему верификации уже обсуждали. Кто проверит верификатор? Кто даст гарантию, что верификатор проверяет семантическую правильность алгоритма , а не формальную?


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 10:35 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 528
Откуда: Казань
Верификатор сам себя проверит. Также как есть компиляторы, которые сами себя компилируют bootstrapping-ом, также можно написать и верификатор, который проверит свой собственный же код, но пока насколько я знаю такого еще нет.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 12:45 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 379
Откуда: Киев
Да, формальное доказательство - это идеал, к которому надо стремиться. И, пожалуй, для критических областей это должно стать нормой. Но попробовав на практике пару существующих решений, должен сказать, что это накладно, а без дополнительного обучения вообще не даётся. Рассчитывать на массовое применение не приходится, поэтому нужны компромиссные решения - не полноценные, но легко пишущиеся.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 12:55 

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 14:39 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 379
Откуда: Киев
Позвольте уточнить - без дополнительного обучения использованию утилиты.
Вот простой пример использования 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 должно быть проще, но там получил то же самое. Нашёл информацию, что есть специальная библиотека, позволяющая доказывать такие вещи, но в свободной поставке я её не нашёл.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 15:01 

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 528
Откуда: Казань
В примере, который вы привели, не указано предусловие, а только постусловие. Предусловие обычно обозначается словом require. Возможно, что из-за этого доказательство не было успешным.


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Вторник, 31 Январь, 2017 15:20 

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


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 12 ] 

Часовой пояс: UTC + 3 часа


Кто сейчас на конференции

Сейчас этот форум просматривают: Google [Bot] и гости: 2


Вы не можете начинать темы
Вы не можете отвечать на сообщения
Вы не можете редактировать свои сообщения
Вы не можете удалять свои сообщения
Вы не можете добавлять вложения

Найти:
Вся информация, размещаемая участниками на конференции (тексты сообщений, вложения и пр.) © 2005-2017, участники конференции «OberonCore», если специально не оговорено иное.
Администрация не несет ответственности за мнения, стиль и достоверность высказываний участников, равно как и за безопасность материалов, предоставляемых участниками во вложениях.
Без разрешения участников и ссылки на конференцию «OberonCore» любое воспроизведение и/или копирование высказываний полностью и/или по частям запрещено.
Powered by phpBB® Forum Software © phpBB Group
Русская поддержка phpBB