|
|
|
assert [2023/12/17 00:51]
comdiv создано |
assert [2023/12/17 04:00] (текущий)
comdiv |
| ''ASSERT(condition: BOOLEAN);'' | ''ASSERT(condition: BOOLEAN);'' |
| |
| Предопределённая процедура ASSERT (assertion — утверждение) нужна для того же, что и встроенные проверки — удостоверять инварианты кода. Главное отличие от встроенных проверок в том, что проверяемые в ASSERT утверждения заданы не самим языком, а спецификацией программы. Код должен строиться исходя из положения, что ASSERT его документирует. Не стоит опираться на то, что в случае ложного условия ход выполнения кода аварийно завершится, даже если генерация такой возможности никогда не выключается при трансляции. Такое поведение нужно для отладки и для предотвращения потенциально опасного дальнейшего выполнения ошибочного кода, но не как часть нормального процесса. | Предопределённая процедура ASSERT (assertion — утверждение) нужна для того же, что и встроенные проверки — удостоверять неизменные свойства кода. Главное отличие от встроенных проверок в том, что проверяемые в ASSERT свойства заданы не самим языком, а спецификацией программы. Код должен строиться исходя из положения, что ASSERT его документирует. Не стоит опираться на то, что в случае ложного условия ход выполнения кода аварийно завершится, даже если генерация такой возможности никогда не выключается при трансляции. Такое поведение нужно для отладки и для предотвращения потенциально опасного дальнейшего выполнения ошибочного кода, но не как часть нормального процесса. |
| |
| При доказательстве корректности кода, если бы оно состоялось, утверждения в ASSERT, так же как и внутренние проверки языка, должны были бы быть удостоверены как истинные ещё до трансляции кода. Главная причина того, что ASSERT проверяется во время исполнения программы, заключается в том, что полная статическая верификация — это трудно воплотимая задача, а динамическая проверка делается чрезвычайно просто. | При доказательстве корректности кода, если бы оно состоялось, утверждения в ASSERT, так же как и внутренние проверки языка, должны были бы подтвердится как истинные ещё до трансляции кода. Главная причина того, что ASSERT проверяются при исполнении программы, заключается в том, что полная статическая верификация — это трудно воплотимая задача, а динамическая проверка делается чрезвычайно просто. |
| | |
| Среди прочего это означает, что ASSERT не предназначен для проверки вводимых извне данных, так как их соответствие внутренним ожиданиям нельзя гарантировать для общего случая. Такое использование ASSERT является либо прямой ошибкой, либо происходит как следствие другой ошибки. Для проверок вводимых данных нужно использовать оператор IF и другие механизмы. | |
| |
| | Среди прочего, это означает, что ASSERT не предназначен для проверки вводимых извне данных, так как их соответствие внутренним ожиданиям нельзя гарантировать для общего случая. Такое использование ASSERT либо само по себе является ошибкой, либо происходит как следствие другой ошибки. Для проверок вводимых данных нужно использовать оператор IF и другие механизмы. |
| |
