Утверждение (программирование)

В следующем примере два утверждения — x > 0 и x > 1 — действительно истинны в отмеченных точках выполнения программы:

x = 1;
assert x > 0;
x++;
assert x > 1;

Используя утверждения, программисты могут явно указывать спецификацию программ и рассуждать о корректности кода. Например, предусловие (утверждение в начале фрагмента кода) определяет множество состояний, при которых, по задумке программиста, должен выполняться данный код; постусловие (размещаемое в конце) определяет ожидаемое состояние после завершения выполнения. Пример: x > 0 { x++ } x > 1.

В приведённом выше примере используется нотация для вставки утверждений, предложенная Чарльзом Энтони Ричардом Хоаром (англ. C. A. R. Hoare) в 1969 году^[1]. Эта нотация не реализована в существующих массовых языках программирования. Однако программисты могут включать непроверяемые утверждения, используя комментарии в исходном коде. Например, в C++:

x = 5;
x = x + 1;
// {x > 1}

Фигурные скобки в комментарии позволяют отличить такие утверждения от других видов комментариев.

Библиотеки также могут предоставлять функциональность утверждений. Например, в языке C с использованием glibc и стандартом C99:

#include <assert.h>

int f(void) {
    int x = 5;
    x = x + 1;
    assert(x > 1);
}

Многие современные языки программирования поддерживают проверяемые утверждения — специальные операторы, которые оцениваются во время выполнения (или, иногда, на этапе компиляции). Если в момент исполнения утверждение возвращает ложь, происходит ошибка утверждения, обычно приводящая к аварийному завершению программы. Это помогает быстро локализовать место обнаружения логической неисправности, что во многих случаях предпочтительнее иным последствиям некорректного хода исполнения.

Использование утверждений способствует проектированию, разработке и формальному анализу корректности программ.

В языках программирования, таких как Eiffel, утверждения являются частью процесса проектирования; в других языках, например C и Java, они чаще используются только для проверки предположений на этапе выполнения. В обоих случаях утверждения могут проверяться во время исполнения, но обычно также могут быть отключены.

Утверждения могут выступать в роли своеобразной документации: они описывают состояние, которое ожидает код перед началом выполнения, и состояние, в которое код должен привести программу после окончания выполнения, а также могут формулировать инварианты класса. Язык Eiffel интегрирует такие утверждения на уровне синтаксиса языка и автоматически извлекает их для документации класса, что составляет основу метода проектирования по контракту.

Этот подход полезен и в языках, не имеющих явной поддержки защитных утверждений: утверждения, встроенные непосредственно в исполняемый код (а не комментарии), позволяют программе проверять их на каждом запуске; если они перестают выполняться, можно сразу обнаружить ошибку. Это предотвращает рассинхронизацию кода и документации.

Утверждение может использоваться для явной проверки предположения, сделанного программистом на этапе написания кода, остаётся ли оно верным при запуске программы. Например, следующий пример на Java:

int total = countNumberOfUsers();
if (total % 2 == 0) {
    // total — чётное
} else {
    // total — нечётное и неотрицательное
    assert total % 2 == 1;
}

В Java оператор % — это оператор остатка (модуля), причём, если первый аргумент отрицателен, результат также может быть отрицательным (в отличие от математического определения остатка). Здесь предполагается, что total всегда неотрицательно, и остаток от деления на 2 равен 0 или 1. Утверждение явно фиксирует это допущение: если countNumberOfUsers вдруг вернёт отрицательное значение, это сигнализирует о логической ошибке.

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

Иногда утверждения помещают туда, куда выполнение никогда не должно попадать. К примеру, утверждение можно разместить в ветке default оператора switch в языках C, C++, Java. Для вариантов, явно не обработанных программистом, будет возбуждаема ошибка и программа завершится, не скрывая ошибочного хода. В языке D соответствующее утверждение добавляется автоматически, если блок switch не содержит default.

В Java утверждения появились в версии 1.4: при ошибке возбуждается AssertionError, если программа запущена с соответствующими флагами. Без них, инструкции assert игнорируются. В C стандартный заголовок assert.h определяет макрос assert(выражение), который прерывает выполнение программы при ложном выражении. В C++ аналогичные макросы определяются как в assert.h, так и в cassert.

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

Использование утверждений облегчает технологии разработки, такие как разработка через тестирование (TDD), даже без сторонних библиотек.

Во время жизненного цикла разработки программу обычно тестируют с включёнными утверждениями. Если срабатывает ошибка утверждения, разработчик сразу узнаёт об этом, а выполнение зачастую приостанавливается. Это удобно, потому что если программа продолжит работу после нарушения условия, она может привести своё состояние к ещё более сложному для диагностики. Информация от системы утверждений (место ошибки, стек вызовов, дамп памяти и др.) позволяет быстро найти причину. Таким образом, утверждения — мощный инструмент отладки.

После развертывания программы в промышленном окружении утверждения, как правило, отключают, чтобы избежать издержек по времени и непредвиденных эффектов. В некоторых случаях (например, C/C++, где используются макросы), утверждения полностью удаляются из конечного кода; в других (например, Java) они физически присутствуют, но могут быть активированы для анализа ошибок у потребителя^[2].

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

Утверждения, проверяемые на этапе компиляции, называются статическими утверждениями.

Статические утверждения особенно полезны для метапрограммирования во время компиляции, но применимы и в низкоуровневых языках (например, C, через создание некорректного кода, если (и только если) утверждение не выполняется). Стандарты C11 и C++11 поддерживают конструкцию static_assert. В версиях C до этого статическое утверждение можно реализовать, например, так:

#define SASSERT(pred) switch(0){case 0:case pred:;}

SASSERT(БУЛЕВОЕ_ВЫРАЖЕНИЕ);

Если часть (БУЛЕВОЕ_ВЫРАЖЕНИЕ) равна ложному, соответствующий код не скомпилируется: компилятор не допускает повторяющихся case-меток. Выражение должно быть вычисляемо на этапе компиляции (например, (sizeof(int)==4)). Этот приём нельзя использовать на уровне файла, он работает только внутри функции.

Другой распространённый способ^[3] реализации статических утверждений на C:

static char const static_assertion[ (БУЛЕВОЕ_ВЫРАЖЕНИЕ)
                                    ? 1 : -1
                                  ] = {'!'};

Если выражение ложно, попытка завести массив отрицательной длины приведёт к ошибке компиляции. Если компилятор разрешает массивы отрицательной длины, то инициализация массивом из одного байта (значение '!') должна привести к ошибке. Как и прежде, выражение должно быть вычислимым во время компиляции (например, (sizeof(int) == 4)).

Оба способа требуют уникальных имён для каждого утверждения. Современные компиляторы поддерживают макрос препроцессора __COUNTER__, который возвращает уникальное число во время обработки файла^[4].

В языке D статические утверждения реализованы как конструкция static assert^[5].

В большинстве языков можно глобально включать и отключать проверки утверждений. Как правило, во время разработки утверждения активны, а для релиза отключаются. Отключение утверждений экономит ресурсы на их вычисление; при условии, что вычисление не имело побочных эффектов на программу, это не меняет корректную логику исполнения. Однако в аномальных случаях отключение проверок позволяет программе продолжить выполнение, тогда как сработавшее утверждение привело бы к остановке — иногда это поведение предпочтительно.

В некоторых языках (например, C, YASS и C++), через препроцессор, утверждения могут быть полностью удалены на этапе компиляции.

Аналогично, запуск интерпретатора Python с параметром -O приводит к тому, что специальные байткод-инструкции для assert не создаются вовсе^[6].

Для Java требуется специальный параметр при запуске, чтобы включить проверки утверждений. Без этого опциональные проверки не выполняются, однако сами выражения assert физически остаются в коде (если их не оптимизировал JIT-компилятор или не обернули в if (false)).

Программисты могут реализовать такие проверки и вручную, не используя синтаксис утверждений.

Утверждения принципиально отличается от стандартных механизмов обработки ошибок. Утверждения обозначают заведомо невозможные по замыслу случаи и обнаруживают ошибки программирования; если «невозможное» случилось — значит, в программе есть фундаментальный дефект. Напротив, обработка ошибок касается ситуаций, которые по крайней мере вероятны теоретически. Использовать утверждения для обычной обработки ошибок не рекомендуется: утверждения не позволяют исправить ошибку, они просто аварийно завершают программу; утверждения могут быть отключены в рабочей сборке; они могут не снабжаться подробным сообщением для пользователя.

Пример использования утверждения для обработки ошибки:

int* ptr = (int*)malloc(sizeof(int) * 10);
assert(ptr);
// далее работа с ptr
...

Здесь программист знает, что malloc может вернуть NULL, если не хватило памяти, а ОС не гарантирует успешность каждого выделения памяти. Если возникла ошибка, программа тут же аварийно завершится. Без этого проверки программа продолжила бы работать, что могло бы привести к ещё более тяжёлым последствиям (например, обращению по NULL-указателю). Но если нужна штатная обработка — например, сервер обслуживает много клиентов или содержит данные, которые должны быть корректно завершены, — лучше предусмотреть явную обработку ошибки вместо assert.

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

Ещё одна версия вышеописанного примера:

int* ptr;
// Строка ниже не выполнится при компиляции с -NDEBUG!
assert(ptr = (int*)malloc(sizeof(int) * 10));
// далее ptr не инициализирован при -NDEBUG!
...

Здесь, если компиляция производится с флагом NDEBU , что считается признаком завершения разработки), строка assert() удаляется, а ptr не инициализируется, что может привести к сегментационному нарушению или другим «скользящим» ошибкам. Некоторые программисты используют аналогичные макросы VERIFY(X) для сокращения таких рисков.

Современные компиляторы могут выдавать предупреждение при анализе такого кода^[7].

В отчётах 1947 года фон Неймана и Голдстайна^[8] по проекту IAS-машины алгоритмы описывались с помощью ранних блок-схем, где встречались и утверждения: «Может быть, что каждый раз, когда C достигает определённой точки в блок-схеме, одна или несколько переменных будут автоматически обладать определёнными значениями, свойствами либо будут удовлетворять определённым взаимосвязям. Мы можем в этой точке специально явно указать эти ограничения. Для этого мы вводим специальные блоки, которые назвали assertion box».

Подход к доказательству корректности программ с применением утверждений продвигал Алан Тьюринг. В лекции «Проверка большой программы» (Cambridge, 24 июня 1949) Тьюринг отмечал: «Как проверить большую программу на корректность? Чтобы облегчить труд проверяющего, программист должен сделать ряд конкретных утверждений, каждое из которых можно проверить отдельно, и, исходя из них, легко убедиться в корректности всей программы»^[9].