OberonCore
https://forum.oberoncore.ru/

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

Автор:  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 не требует этого.

Автор:  Comdiv [ Воскресенье, 27 Декабрь, 2020 23:53 ]
Заголовок сообщения:  Re: Опасный ASSERT

Comdiv писал(а):
Код:
/*@
  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 должно быть проще, но там получил то же самое. Нашёл информацию, что есть специальная библиотека, позволяющая доказывать такие вещи, но в свободной поставке я её не нашёл.
Кстати, этот код доказал другой разработчик, правда, грязно - введением дополнительной аксиоматики. Не уверен, что исходных аксиом не хватало.

Автор:  budden [ Понедельник, 28 Декабрь, 2020 01:47 ]
Заголовок сообщения:  Re: Опасный ASSERT

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

Так вот, до обсуждения ассертов стоило бы спросить, почему для числовых типов потеря данных требует каких-то явных телодвижений, а для строковых оно является умолчанием и происходит легко и непринуждённо? Раньше, когда я пытался построить рекламу "Оберона против С++", тот же Сергей мне справедливо указал, что Оберон создавался не как надёжный язык, а как учебный. В чём-то он случайно оказался надёжнее Си, но это не было целью. Поэтому, если в языке вы получили граблями по лбу, то надо было читать документацию, а не рекламу.

Моя точка зрения остаётся такой, что обрезать данные молча, неявно и по умолчанию - это гораздо хуже любых ассертов. Но я и не оберонщик. Я - за другой, лучший оберон, в котором догмой будет не следование обстоятельствам Вирта и решениям, которые из них вытекали, а дружественность к кибербезопасности и к надёжности оборудования. Оберон близко к этому, но он не в этой точке. Ряд решений, в т.ч. и вот это с COPY, да и некоторые другие, опасны. Я воспринимал Оберон как отправную точку. Просто я уже это забыл, пока возился с A2. А потом вообще увяз в переводе и не факт, что куда-нибудь сдвинусь дальше. Благодарю Сергея за напоминание.

Дальше, там шла речь, что если мы оставим ассерт, то девушка в солярии сварится, и поэтому ассертов в промышленном коде быть не должно, а вместо них должна быть обработка ошибок. Неплохо бы, если бы Сергей ответил на вопрос - а если в соседний дом ударила молния, часть оборудования солярия сгорела, но модуль управления уцелел (возможно, не весь или с изменённым содержимым памяти) - как без исключения (и без рантайм-проверок) об этом можно узнать? Контроллер будет продолжать работать и девушка всё равно сварится.

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

Я считаю, что компьютеры уже настолько значимы в нашей жизни, что ассерты должны оставаться и в промышленной эксплуатации. Да и вообще, расстояние между промышленным и отладочным кодом должно быть минимальным, потому что эти коды могут кардинально отличаться на компиляторах типа gcc. То, что у оберона мало флажков (было изначально) - это прекрасно и нужно стараться это сохранить. Что происходит при падении ассерта - это уже отдельный вопрос.

Автор:  Comdiv [ Понедельник, 28 Декабрь, 2020 03:27 ]
Заголовок сообщения:  Re: Опасный ASSERT

budden писал(а):
Так вот, до обсуждения ассертов стоило бы спросить, почему для числовых типов потеря данных требует каких-то явных телодвижений, а для строковых оно является умолчанием и происходит легко и непринуждённо?
А этот вопрос тоже обсуждался - это произвольный выбор авторов транслятора. У COPY нет обрезательной семантики, а по общему духу при недостатке места должно было быть падение вместо молчаливого урезания. Упорство этому, как и в схожих случаях, лишь результат гордыни - "погромист не должен ошибаться".

budden писал(а):
Но я и не оберонщик. Я - за другой, лучший оберон, в котором догмой будет не следование обстоятельствам Вирта и решениям, которые из них вытекали, а дружественность к кибербезопасности и к надёжности оборудования.
А тут дело не в том, оберонщик вы или не оберонщик, и как понимаете или не понимаете, что делал Вирт. Если Вас интересует защитная семантика, то намекну, что есть, как минимум, один такой транслятор Оберона и воплощение проверок в нём никак не противоречит авторскому описанию языка.

budden писал(а):
Я считаю, что компьютеры уже настолько значимы в нашей жизни, что ассерты должны оставаться и в промышленной эксплуатации
С проверкой утверждений во время исполнения в эксплуатируемом коде всё, несколько, сложнее. Но прояснение этого требует обстоятельного текста.

Автор:  budden [ Понедельник, 28 Декабрь, 2020 12:24 ]
Заголовок сообщения:  Re: Опасный ASSERT

Comdiv писал(а):
есть, как минимум, один такой транслятор Оберона и воплощение проверок в нём никак не противоречит авторскому описанию языка.

Вот был бы я министром промышленности Швейцарии или кто у них там решает, и пришёл бы ко мне Вирт и сказал: «давайте заниматься импортозамещением, вот я язык программирования отечественный придумал, компьютер свой собрал, операционную систему». Я бы почитал такое описание и сказал бы: «многовато у тебя там вещей недоопределено. Взять хотя бы это вот COPY. Ты ведь не язык программирования придумал. А придумал ты семейство языков, мало связанных друг с другом. Если мы все эти языки назовём одним названием, это будет коварное лукавство. Люди начнут по ошибке считать их за один единый язык и портировать свои программы с одной реализации на другую. У нас начнут паровозы с рельсов сходить, у золота в банках ноги вырастут, девушки в соляриях вариться будут еженедельно, а заминированные тоннели в Альпах сами взорвутся. А народ у нас горячий, сам знаешь, горцы, у каждого по ружью. До смертоубийства дойдёт. У кого ж научился ты такому непотребству? На тебя варвары заморские так повлияли со своим "Си" дьяволомерзким? Али ты съездил в Россию в будущий век, где так законы будут писать, чтобы дышло поудобнее получилось? Вспомни, Николай, что ты Швейцарец! Наши часы самые точные, а наши топоры никогда не слетают с ручки! Не позорь Родину, иди и доделай до нормального описания языка!»

Автор:  Ярослав Романченко [ Понедельник, 28 Декабрь, 2020 12:35 ]
Заголовок сообщения:  Re: Опасный ASSERT

Проблема вовсе не в COPY, а в том, что надо заранее предусматривать, что данных может оказаться больше и пользоваться тогда не COPY, а каким-нибудь StringBuilder-ом. Но с другой стороны может стоять другое требование, что нужно вообще не использовать память на куче или минимизировать её использование! Тогда никакой StringBuilder не подходит и надо банально объявить статические массивы больших размеров и таки пользоваться COPY. Нужно подобные решения продумывать в каждом конкретном случае.
Вы не любите строки в Оберон-е? Просто их надо уметь готовить :)

Автор:  Ярослав Романченко [ Понедельник, 28 Декабрь, 2020 13:38 ]
Заголовок сообщения:  Re: Опасный ASSERT

А то, что проблемы возникают при использовании символов Unicode. Так это ещё исторически сложилось со времён ETH Oberon. Там вообще не предусматривалось никакой интернационализации системы. Такого "багажа" уже немного, но время от времени встречается, и, конечно, надо от него избавляться.

Автор:  Comdiv [ Понедельник, 28 Декабрь, 2020 15:42 ]
Заголовок сообщения:  Re: Опасный ASSERT

budden писал(а):
Вот был бы я министром промышленности Швейцарии или кто у них там решает
Слава богу, что это не так, потому что решать Вам ничего нельзя :mrgreen: . Вы даже приписываете Вирту решения, которые имеют к нему такое же отношение, как ЯОС.

budden писал(а):
Не позорь Родину, иди и доделай до нормального описания языка!»
Много раз писал, что авторское описание языка - это не стандарт языка. И как для авторского описания оно сделано достаточно хорошо. То, что от него требуют большего, это больше вопрос к требующим.

Конечно, приятно, когда всё уже готово, да так как тебе надо, но на самом деле стандарт должны были бы написать представители сообщества. И одним человеком стандарт никогда не делается. Но перспективы договориться по этому вопросу можете оценить по дискуссиям по COPY и ASSERT.

Автор:  Comdiv [ Понедельник, 28 Декабрь, 2020 15:43 ]
Заголовок сообщения:  Re: Опасный ASSERT

Ярослав Романченко писал(а):
Проблема вовсе не в COPY, а в том, что надо заранее предусматривать
Это ведь пересказ обобщённого "программист не должен ошибаться".

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