Утверждение (разработка программного обеспечения)

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

В последнем случае некоторые программы проверяют утверждения, фактически оценивая предикат во время их выполнения. Затем, если это на самом деле не так (сбой утверждения), программа считает себя сломанной и обычно намеренно аварийно завершает работу сбоя утверждения или выдает исключение .

Подробности

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

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

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

В приведенном выше примере используются обозначения для включения утверждений, использованные К. А. Хоаром в его статье 1969 года. ^[1] Эту нотацию нельзя использовать в существующих основных языках программирования. Однако программисты могут включать непроверяемые утверждения, используя функцию комментариев своего языка программирования. Например, в С++ :

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 is even
 } else {
     // total is odd and non-negative
     assert total % 2 == 1;
 }

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

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

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

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

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

Конструкции утверждений в языке позволяют упростить разработку через тестирование (TDD) без использования сторонней библиотеки.

Утверждения во время цикла разработки

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

Утверждения в производственной среде

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

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

Статические утверждения

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

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

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

SASSERT( BOOLEAN CONDITION );

Если (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);
  assert(ptr);
  // use ptr
  ...

Здесь программист знает, что malloc вернет NULL указатель , если память не выделена. Это возможно: операционная система не гарантирует, что каждый вызов malloc получится. Если произойдет ошибка нехватки памяти, программа немедленно прервется. Без утверждения программа продолжала бы работать до тех пор, пока ptr было разыменовано и, возможно, дольше, в зависимости от конкретного используемого оборудования. Пока утверждения не отключены, немедленный выход гарантирован. Но если требуется корректный сбой, программа должна его обработать. Например, сервер может иметь несколько клиентов или может содержать ресурсы, которые не будут освобождены полностью, или на нем могут быть незафиксированные изменения для записи в хранилище данных. В таких случаях лучше провалить одну транзакцию, чем резко прервать ее.

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

Рассмотрим еще одну версию предыдущего примера:

  int *ptr;
  // Statement below fails if malloc() returns NULL,
  // but is not executed at all when compiling with -NDEBUG!
  assert(ptr = malloc(sizeof(int) * 10));
  // use ptr: ptr isn't initialised when compiling with -NDEBUG!
  ...

Это может выглядеть как разумный способ присвоить возвращаемое значение malloc к ptr и проверьте, так ли это NULL за один шаг, но malloc звонок и задание ptr является побочным эффектом вычисления выражения, которое формирует assert состояние. Когда NDEBUG параметр передается компилятору, поскольку, когда программа считается безошибочной и выпущенной, параметр assert() утверждение удалено, поэтому malloc() не вызывается, рендеринг ptr неинициализированный. Потенциально это может привести к ошибке сегментации или аналогичной ошибке нулевого указателя гораздо дальше по ходу выполнения программы, вызывая ошибки, которые могут носить спорадический характер и/или их трудно отследить. Программисты иногда используют аналогичное определение VERIFY(X), чтобы облегчить эту проблему.

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

История

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

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

См. также

Ссылки

^ CAR Hoare , Аксиоматическая основа компьютерного программирования , Communications of ACM , 1969.
^ Программирование с использованием утверждений , включение и отключение утверждений
^ Джон Джаггер, Утверждения времени компиляции на C , 1999.
^ GNU, «Серия выпусков GCC 4.3 — изменения, новые функции и исправления»
^ «Статические утверждения» . D Справочник по языку . Фонд языка D. Проверено 16 марта 2022 г.
^ Официальная документация Python, утверждение утверждения
^ «Параметры предупреждения (с использованием коллекции компиляторов GNU (GCC))» .
^ Голдстайн и фон Нейман. «Планирование и кодирование задач для электронного вычислительного прибора». Архивировано 12 ноября 2018 г. в Wayback Machine . Часть II, том I, 1 апреля 1947 г., с. 12.
^ Алан Тьюринг. Проверка большой программы , 1949 год; Цитируется в CAR Hoare, «Старая одежда императора», лекция на премию Тьюринга 1980 года.

Внешние ссылки

Исторический взгляд на проверку утверждений во время выполнения при разработке программного обеспечения Лори А. Кларк, Дэвид С. Розенблюм в: ACM SIGSOFT Software Engineering Notes 31 (3): 25-37, 2006 г.
Утверждения: личный взгляд К.АР. Хоара в: IEEE Annals of the History of Computing, Том: 25, Выпуск: 2 (2003), Страницы: 14–25
«Мой компилятор меня не понимает» , Пол-Хеннинг Камп, ACM Queue 10(5), май 2012 г.
Использование утверждений Джона Регера

[1] CAR Hoare , Аксиоматическая основа компьютерного программирования , Communications of ACM , 1969.

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

[3] Джон Джаггер, Утверждения времени компиляции на C , 1999.

[4] GNU, «Серия выпусков GCC 4.3 — изменения, новые функции и исправления»

[5] «Статические утверждения» . D Справочник по языку . Фонд языка D. Проверено 16 марта 2022 г.

[6] Официальная документация Python, утверждение утверждения

[7] «Параметры предупреждения (с использованием коллекции компиляторов GNU (GCC))» .

[8] Голдстайн и фон Нейман. «Планирование и кодирование задач для электронного вычислительного прибора». Архивировано 12 ноября 2018 г. в Wayback Machine . Часть II, том I, 1 апреля 1947 г., с. 12.

[9] Алан Тьюринг. Проверка большой программы , 1949 год; Цитируется в CAR Hoare, «Старая одежда императора», лекция на премию Тьюринга 1980 года.

[1]

[2]

[3]

[4]

[5]

[6]

[7]

[8]

[9]