Использование ASSERT для проверки корректности [Оберон / Компонентный Паскаль / Вики]

Эта страница только для чтения. Вы можете посмотреть её исходный текст, но не можете его изменить. Сообщите администратору, если считаете, что это неправильно.

====== Использование ASSERT для проверки корректности ======

''ASSERT(condition: BOOLEAN);''

Предопределённая процедура ASSERT (assertion — утверждение) нужна для того же, что и встроенные проверки — удостоверять неизменные свойства кода. Главное отличие от встроенных проверок в том, что проверяемые в ASSERT свойства заданы не самим языком, а спецификацией программы. Код должен строиться исходя из положения, что ASSERT его документирует. Не стоит опираться на то, что в случае ложного условия ход выполнения кода аварийно завершится, даже если генерация такой возможности никогда не выключается при трансляции. Такое поведение нужно для отладки и для предотвращения потенциально опасного дальнейшего выполнения ошибочного кода, но не как часть нормального процесса — ASSERT не имеет отношения к механизму исключений.

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

Среди прочего, это означает, что ASSERT не предназначен для проверки вводимых извне данных, так как их соответствие внутренним ожиданиям нельзя гарантировать для общего случая. Такое использование ASSERT либо само по себе является ошибкой, либо происходит как следствие другой ошибки. Для проверок вводимых данных нужно использовать оператор IF и другие механизмы.

Инструменты пользователя

Инструменты сайта

Инструменты страницы