OberonCore

Библиотека  Wiki  Форум  BlackBox  Компоненты  Проекты
Текущее время: Среда, 27 Январь, 2021 18:54

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




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

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

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

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


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

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


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

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


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

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

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

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


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

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


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

Зарегистрирован: Пятница, 13 Март, 2009 16:36
Сообщения: 955
Откуда: Казань
В книге "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
Сообщения: 1134
Откуда: СССР v2.0 rc 1
Рифат -- последовательный сторонник программирования под доказательство))
Вот ждал, что обязательно здесь подпишется!))
Проблему верификации уже обсуждали. Кто проверит верификатор? Кто даст гарантию, что верификатор проверяет семантическую правильность алгоритма , а не формальную?


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

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


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

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


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

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


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

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


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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Воскресенье, 27 Декабрь, 2020 23:53 

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


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

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

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

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

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

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

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Понедельник, 28 Декабрь, 2020 03:27 

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1165
Откуда: Киев
budden писал(а):
Так вот, до обсуждения ассертов стоило бы спросить, почему для числовых типов потеря данных требует каких-то явных телодвижений, а для строковых оно является умолчанием и происходит легко и непринуждённо?
А этот вопрос тоже обсуждался - это произвольный выбор авторов транслятора. У COPY нет обрезательной семантики, а по общему духу при недостатке места должно было быть падение вместо молчаливого урезания. Упорство этому, как и в схожих случаях, лишь результат гордыни - "погромист не должен ошибаться".

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

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


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

Зарегистрирован: Понедельник, 11 Сентябрь, 2017 13:23
Сообщения: 1180
Comdiv писал(а):
есть, как минимум, один такой транслятор Оберона и воплощение проверок в нём никак не противоречит авторскому описанию языка.

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Понедельник, 28 Декабрь, 2020 12:35 
Аватара пользователя

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


Вернуться к началу
 Профиль  
 
 Заголовок сообщения: Re: Опасный ASSERT
СообщениеДобавлено: Понедельник, 28 Декабрь, 2020 13:38 
Аватара пользователя

Зарегистрирован: Пятница, 11 Май, 2007 21:57
Сообщения: 1443
Откуда: Украина, Киев
А то, что проблемы возникают при использовании символов Unicode. Так это ещё исторически сложилось со времён ETH Oberon. Там вообще не предусматривалось никакой интернационализации системы. Такого "багажа" уже немного, но время от времени встречается, и, конечно, надо от него избавляться.


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

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

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

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


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

Зарегистрирован: Четверг, 08 Май, 2008 19:13
Сообщения: 1165
Откуда: Киев
Ярослав Романченко писал(а):
Проблема вовсе не в COPY, а в том, что надо заранее предусматривать
Это ведь пересказ обобщённого "программист не должен ошибаться".


Вернуться к началу
 Профиль  
 
Показать сообщения за:  Поле сортировки  
Начать новую тему Ответить на тему  [ Сообщений: 32 ]  На страницу 1, 2  След.

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


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

Сейчас этот форум просматривают: нет зарегистрированных пользователей и гости: 1


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

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