В программировании , особенно при использовании парадигмы императивного программирования , утверждение — это предикат ( функция с булевым значением над пространством состояний , обычно выражаемая как логическое предложение с использованием переменных программы), связанный с точкой в программе, которая всегда должна оцениваться как истина в этой точке выполнения кода. Утверждения могут помочь программисту прочитать код, помочь компилятору скомпилировать его или помочь программе обнаружить свои собственные дефекты.
Для последнего некоторые программы проверяют утверждения, фактически оценивая предикат во время выполнения. Затем, если он на самом деле не истинен — ошибка утверждения — программа считает себя сломанной и обычно намеренно аварийно завершает работу или выдает исключение ошибки утверждения .
Следующий код содержит два утверждения, x > 0и x > 1, и они действительно истинны в указанных точках во время выполнения:
x = 1 ; утверждать x > 0 ; x ++ ; утверждать x > 1 ; Программисты могут использовать утверждения, чтобы помочь определить программы и рассуждать о корректности программ. Например, предварительное условие — утверждение, размещенное в начале раздела кода, — определяет набор состояний, при которых программист ожидает выполнения кода. Постусловие — размещенное в конце — описывает ожидаемое состояние в конце выполнения. Например: x > 0 { x++ } x > 1.
В приведенном выше примере используется нотация для включения утверждений, использованная CAR Hoare в его статье 1969 года. [1] Эта нотация не может использоваться в существующих основных языках программирования. Однако программисты могут включать непроверенные утверждения, используя функцию комментариев своего языка программирования. Например, в C++ :
х = 5 ; х = х + 1 ; // {х > 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 — %оператор остатка ( modulo ), и в Java, если его первый операнд отрицательный, результат также может быть отрицательным (в отличие от modulo, используемого в математике). Здесь программист предположил, что 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)часть оценивается как ложная, то приведенный выше код не будет компилироваться, поскольку компилятор не разрешит две метки case с одной и той же константой. Булевое выражение должно быть константным значением времени компиляции, например, было бы допустимым выражением в этом контексте. Эта конструкция не работает в области действия файла (т. е. не внутри функции), поэтому она должна быть обернута внутри функции.(sizeof(int)==4)
Другой популярный [3] способ реализации утверждений в языке C:
static char const static_assertion [ ( БУЛЕВО УСЛОВИЕ ) ? 1 : -1 ] = { '!' }; Если (BOOLEAN CONDITION)часть оценивается как ложная, то приведенный выше код не будет компилироваться, поскольку массивы не могут иметь отрицательную длину. Если на самом деле компилятор допускает отрицательную длину, то байт инициализации ( '!'часть) должен вызывать жалобы даже у таких слишком снисходительных компиляторов. Булево выражение должно быть константным значением времени компиляции, например, (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 ); assert ( ptr ); // используем ptr ... Здесь программист знает, что mallocвернет NULLуказатель, если память не выделена. Это возможно: операционная система не гарантирует, что каждый вызов mallocбудет успешным. Если возникает ошибка нехватки памяти, программа немедленно прервется. Без утверждения программа будет продолжать работать до тех пор, пока ptrне будет разыменована, и, возможно, дольше, в зависимости от конкретного используемого оборудования. Пока утверждения не отключены, гарантируется немедленный выход. Но если требуется изящный сбой, программа должна обработать сбой. Например, сервер может иметь несколько клиентов или может удерживать ресурсы, которые не будут освобождены чисто, или у него могут быть незафиксированные изменения для записи в хранилище данных. В таких случаях лучше допустить сбой одной транзакции, чем внезапно прервать ее.
Другая ошибка — полагаться на побочные эффекты выражений, используемых в качестве аргументов утверждения. Всегда следует помнить, что утверждения могут вообще не выполняться, поскольку их единственная цель — проверить, что условие, которое всегда должно быть истинным, действительно выполняется. Следовательно, если программа считается безошибочной и выпущенной, утверждения могут быть отключены и больше не будут оцениваться.
Рассмотрим еще одну версию предыдущего примера:
int * 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]