В компьютерном программировании , особенно при использовании парадигмы императивного программирования , утверждение — это предикат ( булева функция в пространстве состояний , обычно выражаемая как логическое предложение с использованием переменных программы), связанный с точкой в программе, которая всегда должно оцениваться как true на этом этапе выполнения кода. Утверждения могут помочь программисту прочитать код, помочь компилятору его скомпилировать или помочь программе обнаружить свои собственные дефекты.
В последнем случае некоторые программы проверяют утверждения, фактически оценивая предикат во время их выполнения. Затем, если на самом деле это не так (сбой утверждения), программа считает себя сломанной и обычно намеренно аварийно завершает работу или выдает исключение сбоя утверждения .
Следующий код содержит два утверждения x > 0и x > 1, и они действительно истинны в указанных точках во время выполнения:
х = 1 ; утверждать x > 0 ; х ++ ; утверждать x > 1 ; Программисты могут использовать утверждения, чтобы помочь специфицировать программы и рассуждать о их корректности. Например, предварительное условие — утверждение, помещенное в начало раздела кода — определяет набор состояний, в которых программист ожидает выполнения кода. Постусловие , помещенное в конце, описывает ожидаемое состояние в конце выполнения. Например: x > 0 { x++ } x > 1.
В приведенном выше примере используются обозначения для включения утверждений, использованные К. А. Хоаром в его статье 1969 года. [1] Эту нотацию нельзя использовать в существующих основных языках программирования. Однако программисты могут включать непроверяемые утверждения, используя функцию комментариев своего языка программирования. Например, в С++ :
х = 5 ; х = х + 1 ; // {х > 1} Фигурные скобки, включенные в комментарий, помогают отличить это использование комментария от других его применений.
Библиотеки также могут предоставлять функции утверждения. Например, в C с использованием glibc с поддержкой C99:
#include <assert.h> int f ( void ) { int x знак равно 5 ; х = х + 1 ; утверждать ( х > 1 ); } Некоторые современные языки программирования включают проверяемые утверждения – утверждения , которые проверяются во время выполнения , а иногда и статически. Если во время выполнения утверждение оценивается как ложное, происходит сбой утверждения, что обычно приводит к прерыванию выполнения. Это привлекает внимание к месту, в котором обнаружено логическое несоответствие, и может быть предпочтительнее поведения, которое могло бы возникнуть в противном случае.
Использование утверждений помогает программисту проектировать, разрабатывать и рассуждать о программе.
В таких языках, как Eiffel , утверждения составляют часть процесса проектирования; другие языки, такие как C и Java , используют их только для проверки предположений во время выполнения . В обоих случаях их достоверность можно проверить во время выполнения, но обычно их также можно подавить.
Утверждения могут функционировать как форма документации: они могут описывать состояние, которое код ожидает найти перед запуском (его предварительные условия ), и состояние, в котором код ожидает получить результат после завершения работы ( постусловия ); они также могут указывать инварианты класса . Eiffel интегрирует такие утверждения в язык и автоматически извлекает их для документирования класса. Это составляет важную часть метода проектирования по контракту .
Этот подход также полезен в языках, которые не поддерживают его явно: преимущество использования операторов утверждения вместо утверждений в комментариях состоит в том, что программа может проверять утверждения при каждом запуске; если утверждение больше не выполняется, можно сообщить об ошибке. Это предотвращает рассинхронизацию кода с утверждениями.
Утверждение может использоваться для проверки того, что предположение, сделанное программистом во время реализации программы, остается действительным при выполнении программы. Например, рассмотрим следующий код Java :
int total = countNumberOfUsers (); if ( total % 2 == 0 ) { // общая сумма четная } else { // общая сумма нечетная и неотрицательная . } В Java — %оператор остатка ( по модулю ), а в Java, если его первый операнд отрицательный, результат также может быть отрицательным (в отличие от модуля, используемого в математике). Здесь программист предположил, что totalчисло неотрицательно, так что остаток от деления на 2 всегда будет равен 0 или 1. Утверждение делает это предположение явным: если countNumberOfUsersоно возвращает отрицательное значение, в программе может быть ошибка.
Основным преимуществом этого метода является то, что когда ошибка все же возникает, она обнаруживается немедленно и напрямую, а не позже, благодаря часто неясным последствиям. Поскольку ошибка утверждения обычно сообщает о местонахождении кода, часто можно точно определить ошибку без дальнейшей отладки.
Утверждения также иногда размещаются в точках, которых выполнение не должно достигать. Например, утверждения могут быть размещены в defaultпредложении оператора switchна таких языках, как C , C++ и Java . Любой случай, который программист намеренно не обработает, вызовет ошибку, и программа прервется, а не продолжит молча продолжать работу в ошибочном состоянии. В D такое утверждение добавляется автоматически, если switchутверждение не содержит defaultпредложения.
В Java утверждения являются частью языка начиная с версии 1.4. Ошибки утверждения приводят к возникновению ошибки, AssertionErrorкогда программа запускается с соответствующими флагами, без которых утверждения утверждения игнорируются. В C они добавляются стандартным заголовком, assert.hопределяющим как макрос, который сигнализирует об ошибке в случае сбоя, обычно завершая программу. В C++ оба заголовка и предоставляют макрос. assert (assertion) assert.hcassertassert
Опасность утверждений состоит в том, что они могут вызывать побочные эффекты, изменяя данные в памяти или изменяя время выполнения потока. Утверждения следует реализовывать осторожно, чтобы они не вызывали побочных эффектов в программном коде.
Конструкции утверждений в языке позволяют упростить разработку через тестирование (TDD) без использования сторонней библиотеки.
Во время цикла разработки программист обычно запускает программу с включенными утверждениями. При возникновении сбоя утверждения программист немедленно уведомляется о проблеме. Многие реализации утверждений также останавливают выполнение программы: это полезно, поскольку, если программа продолжает работать после того, как произошло нарушение утверждения, это может испортить ее состояние и затруднить обнаружение причины проблемы. Используя информацию, предоставленную сбоем утверждения (например, место сбоя и, возможно, трассировку стека или даже полное состояние программы, если среда поддерживает дампы ядра или если программа выполняется в отладчике ) , программист обычно может исправить проблема. Таким образом, утверждения предоставляют очень мощный инструмент отладки.
Когда программа развертывается в рабочей среде , утверждения обычно отключаются, чтобы избежать каких-либо накладных расходов или побочных эффектов, которые они могут иметь. В некоторых случаях утверждения полностью отсутствуют в развернутом коде, например, в утверждениях C/C++ через макросы. В других случаях, например в Java, утверждения присутствуют в развернутом коде и могут быть включены в поле для отладки. [2]
Утверждения также могут использоваться, чтобы пообещать компилятору, что данное граничное условие на самом деле недостижимо, тем самым позволяя выполнить определенные оптимизации , которые в противном случае были бы невозможны. В этом случае отключение утверждений может фактически снизить производительность.
Утверждения, которые проверяются во время компиляции, называются статическими утверждениями.
Статические утверждения особенно полезны при метапрограммировании шаблонов времени компиляции , но их также можно использовать в языках низкого уровня, таких как C, путем введения недопустимого кода, если (и только если) утверждение терпит неудачу. C11 и C++11 поддерживают статические утверждения непосредственно через static_assert. В более ранних версиях C статическое утверждение можно реализовать, например, так:
#define SASSERT(pred) switch(0){case 0:case pred:;}SASSERT ( БУЛЕВОЕ УСЛОВИЕ ); Если (BOOLEAN CONDITION)часть оценивается как ложная, приведенный выше код не будет скомпилирован, поскольку компилятор не допустит двух меток регистра с одной и той же константой. Логическое выражение должно быть постоянным значением времени компиляции, например, оно будет допустимым выражением в этом контексте. Эта конструкция не работает в области файла (т. е. не внутри функции), поэтому ее необходимо заключить внутрь функции.(sizeof(int)==4)
Другой популярный [3] способ реализации утверждений в C:
static char const static_assertion [ ( BOOLEAN CONDITION ) ? 1 : -1 ] = { '!' }; Если (BOOLEAN CONDITION)значение части равно false, приведенный выше код не будет скомпилирован, поскольку массивы не могут иметь отрицательную длину. Если на самом деле компилятор допускает отрицательную длину, то байт инициализации (часть '!') должен вызывать недовольство даже таких чрезмерно снисходительных компиляторов. Логическое выражение должно быть постоянным значением времени компиляции, например, оно (sizeof(int) == 4)будет допустимым выражением в этом контексте.
Оба этих метода требуют метода создания уникальных имен. Современные компиляторы поддерживают __COUNTER__определение препроцессора, которое облегчает создание уникальных имен, возвращая монотонно возрастающие числа для каждой единицы компиляции. [4]
D предоставляет статические утверждения посредством использования static assert. [5]
Большинство языков позволяют включать и отключать утверждения глобально, а иногда и независимо. Утверждения часто включаются во время разработки и отключаются во время окончательного тестирования и при выпуске для клиента. Отсутствие проверки утверждений позволяет избежать затрат на их оценку, хотя (при условии, что утверждения не имеют побочных эффектов ) по-прежнему дает тот же результат в нормальных условиях. В аномальных условиях отключение проверки утверждений может означать, что программа, которая могла быть прервана, продолжит работу. Иногда это предпочтительнее.
Некоторые языки, включая C , YASS и C++ , могут полностью удалять утверждения во время компиляции с помощью препроцессора .
Аналогичным образом, запуск интерпретатора Python с «-O» (для «оптимизировать») в качестве аргумента приведет к тому, что генератор кода Python не будет выдавать какой-либо байт-код для утверждений. [6]
Java требует, чтобы опция была передана механизму времени выполнения, чтобы включить утверждения. При отсутствии этой опции утверждения обходятся, но они всегда остаются в коде, если только они не оптимизированы JIT-компилятором во время выполнения или не исключены во время компиляции , когда программист вручную помещает каждое утверждение за предложением if (false).
Программисты могут встраивать в свой код проверки, которые всегда активны, обходя или манипулируя обычными механизмами проверки утверждений языка.
Утверждения отличаются от обычной обработки ошибок . Утверждения документируют логически невозможные ситуации и обнаруживают ошибки программирования: если происходит невозможное, то с программой явно что-то не так. Это отличается от обработки ошибок: возможно большинство ошибок, хотя возникновение некоторых из них на практике крайне маловероятно. Использование утверждений в качестве универсального механизма обработки ошибок неразумно: утверждения не позволяют восстанавливаться после ошибок; ошибка утверждения обычно резко останавливает выполнение программы; и утверждения часто отключаются в рабочем коде. Утверждения также не отображают понятное для пользователя сообщение об ошибке.
Рассмотрим следующий пример использования утверждения для обработки ошибки:
int * ptr = malloc ( sizeof ( int ) * 10 ); утверждать ( ptr ); // используем PTR ... Здесь программист знает, что mallocвернет NULLуказатель , если память не выделена. Это возможно: операционная система не гарантирует, что каждый вызов mallocбудет успешным. Если произойдет ошибка нехватки памяти, программа немедленно прервется. Без этого утверждения программа продолжала бы работать до тех пор, пока ptrне будет разыменована, а возможно, и дольше, в зависимости от конкретного используемого оборудования. Пока утверждения не отключены, немедленный выход гарантирован. Но если требуется корректный сбой, программа должна его обработать. Например, сервер может иметь несколько клиентов или может содержать ресурсы, которые не будут освобождены полностью, или на нем могут быть незафиксированные изменения для записи в хранилище данных. В таких случаях лучше провалить одну транзакцию, чем резко прервать ее.
Другая ошибка — полагаться на побочные эффекты выражений, используемых в качестве аргументов утверждения. Всегда следует помнить, что утверждения могут вообще не выполняться, поскольку их единственная цель — проверить, что условие, которое всегда должно быть истинным, на самом деле выполняется. Следовательно, если программа считается безошибочной и выпущена, утверждения могут быть отключены и больше не будут оцениваться.
Рассмотрим еще одну версию предыдущего примера:
интервал * ПТР ; // Приведенный ниже оператор не выполняется, если malloc() возвращает NULL, // но не выполняется вообще при компиляции с -NDEBUG! Assert ( ptr = malloc ( sizeof ( int ) * 10 )); // используем ptr: ptr не инициализируется при компиляции с -NDEBUG! ... Это может показаться разумным способом присвоить возвращаемое значение mallocи ptrпроверить, находится ли оно NULLза один шаг, но mallocвызов и присвоение ptr— это побочный эффект вычисления выражения, формирующего assertусловие. Когда NDEBUGпараметр передается компилятору, например, когда программа считается безошибочной и выпущенной, assert()оператор удаляется и поэтому malloc()не вызывается, что делает его ptrнеинициализированным. Потенциально это может привести к ошибке сегментации или аналогичной ошибке нулевого указателя гораздо дальше по ходу выполнения программы, вызывая ошибки, которые могут носить спорадический характер и/или их трудно отследить. Программисты иногда используют аналогичное определение VERIFY(X), чтобы облегчить эту проблему.
Современные компиляторы могут выдать предупреждение при обнаружении приведенного выше кода. [7]
В отчетах 1947 года фон Неймана и Голдстайна [8] о конструкции машины IAS они описывали алгоритмы, используя раннюю версию блок-схем , в которые включали утверждения: «Возможно, это правда, что всякий раз, когда C действительно достигает определенной точки на блок-схеме одна или несколько связанных переменных обязательно будут обладать определенными указанными значениями, или обладать определенными свойствами, или удовлетворять определенным свойствам друг друга. Кроме того, в такой момент мы можем указать действительность этих ограничений. По этой причине мы будем обозначать каждую область, в которой подтверждается обоснованность таких ограничений, специальным полем, которое мы называем полем утверждения».
Метод утверждений для доказательства правильности программ был предложен Аланом Тьюрингом . В докладе «Проверка большой процедуры» в Кембридже 24 июня 1949 года Тьюринг предположил: «Как можно проверить большую программу в смысле уверенности в ее правильности? Для того, чтобы у человека, проверяющего, не было слишком трудных задач, задаче программист должен сделать ряд определенных утверждений , которые можно проверить индивидуально и из которых легко вытекает корректность всей программы». [9]