Виды постоянных

1. По способу введения выделяются:
   1. Непосредственные значения
   2. Константные выражения
   3. Неявные константные выражения
   4. Именованные постоянные
2. По заменяемости значения делятся на:
   1. Обычные константы
   2. Параметрические постоянные

1.1 Непосредственные значения

Это положительные целые, точные и приблизительные положительные дроби, расширенные идентификаторы, и логические значения true и false.

1.2. Константные выражения

Это выражения, в которых все операнды тоже постоянные, как непосредственные значения так и подвыражения. Вызов константной функции с константными фактическими параметрами, разумеется, тоже является константным выражением.

1.3. Неявно постоянные выражения (непрозрачные константы)

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

1.4. Именованные

Именованные постоянные появлются как итог создания объявления в отделе для постоянных подпрограммы или раздела.

2.1. Обычные константы

Cмысл обычных констант неразрывно связан с их значением. Такие постоянные нет необходимости менять между трансляциями. Конечно, значение объявлений могут меняться из-за редактирования, но считается, что это меняет смысл кода, а не является свойством объявлений. Примером обычных констант являются приблизительные значения физических и математических постоянных.

2.2. Параметрические постоянные

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

Принципиальная разница между постояным параметром и обычной константой проявляется в анализе. Если истинно константное выражение в качестве условия ветвления считается ошибочным состоянием, поскольку свидетельсвует об ошибке — бессодержательности проверки и возможном наличии недостижимого кода, то аналогичное использование параметров-постоянных трансляции может быть полезным, и не считается ошибкой.

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

1. Непосредственные значения — всегда обычные константы
2. Константное выражение является параметрическим, если оно содержит хотя бы один параметрический операнд
3. Именованная константа является параметрической, если
   • В определении ей задано параметрическое выражение
   • Или её имя импортировоано из раздела, где оно экспортировано с меткой ограниченного экспорта по имени
4. Аналогично, константная функция даёт параметрическое значение, если
   • В определении она использует хотя бы одно параметрическое выражение
   • Или функция импортирована из раздела, где она экспортирована с меткой ограниченного экспорта по имени

Разновидности состояния переменной

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

Следует учитывать, что статическая и динамическая характеристики могут не совпадать вследствии циклов и ветвлений. Кроме того, противоположные характеристики значения, которые не могут совпадать в переменной во времени, то есть динамически, статически могут присутстсвовать в одном месте кода в качестве возможности вследствии неопределённости.

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

1. По возможности менять значение
   1. Неизменяемое значение
   2. Запрещённое для изменения значения в контексте
   3. Не запрещённое для изменения
2. По очевидности значения
   1. Известное значение
   2. Неизвестное
3. По использованию значения
   1. Прочитанное значение
   2. Неиспользованное значение
4. По широте множества значения
   1. Нормальное значение — значение в границах применимости типа-основы, полученное без ошибок кода
   1. Неявно ограниченное
   2. Произвольное значение исходного типа
   2. Без значения
   1. Не выставлено начальное значение
   2. Значение устранено в результате его односторонней передачи или закрытия
   3. Ошибочное значение, полученное как следствие проявление ошибки в коде.
5. По защите значения от утечки
   1. Незащищённое по умолчанию
   2. Защищённое по явному указанию
6. По уникальности значения
   1. Гарантируется, что значение уникально в указанном контексте
   2. Значение может быть не уникально
   3. Значение, изолированное в графе

По изменяемости

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

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

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

По очевидности значения

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

По использованию

Значение из переменной в итоге может быть не использовано, что считается ошибкой, если код ни при каких обстоятельствах не подразумевает его прочтения. Если значение действительно не нужно, что может произойти, например, при получении второстепенного значения из некой процедуры, то вместо объявленной переменной лучше использовать предопределённое имя unused. Но если выходное значение не было помечено, как дозволенное для пропуска, то это имя недопустимо.

По множеству значений

Нормальное значение может быть произвольным или ограниченным, явно или неявно.

Зачастую, основной тип переменной указывается достаточно грубо, избыточно широко задавая множество возможных значений, в то время как действительное множество у́же. Но сверхстрогое указание типа, что было бы полезно с точки зрения доказательства правильности кода, требует слишком больших усилий, поэтому не может быть обязательным в прагматичном языке. Тем не менее, по умолчанию это более узкое подмножество подразумевается неявно, что важно для анализа кода. Но в ряде случаев важно подчеркнуть, что указываемый тип не является приблизительным, а действительно задаёт всё поразумеваемое за ним множество. Например, это характерно для вводимых данных и генераторов псевдослучайных чисел.

Первоначально, произвольность значения задаётся уточнением типа переменной — приставкой any, но также произвольность можно передать с помощью части выражений. С другой стороны произвольность снимается в ветвлении после применения в логических выражениях. Также произвольность может исчезать в некоторых выражениях, например, при делении произвольного значения.

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

Отсутствие значения у переменной означает лишь отсутствие явно заданного значения. Чтение переменной в этом состоянии считается ошибочным состоянием.

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

По защите значения от утечки

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

По уникальности значения

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

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

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

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

Свойства. Доказуемый

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

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

Утверждения

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

// например 
! a > b;

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

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

Выражение в утверждении в правильном коде должно оставаться всегда истинным, и только из-за ошибок в коде оно может оказаться ложным. Ложь в утверждении является ошибочным состоянием.

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

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

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

Присваивание

Разновидности

• Обычное var := expr — только устанавливает значение переменной
• Завершающее var = expr — устанавливает значение и маркирует конец возможности изменения переменной ниже по тексту в тех же ветках кода, учитывая вложенность.
• Обмен var1 <-> var2 — взаимный обмен переменных значениями
• Передающее var1 <- var2 — подразумевает, что правая переменная теряет значение
• Лишение значения X var — обозначение, что переменная утратила значение

Внутриструктурность присваивания — var.{a := b}. Аналогично var.a := var.b за исключением того, что позволяет удостоверять сохранение полноты графа. Внутриструктурность неприменима только к лишению значения.

proc go(x, y int) (ok bool) {
 var (last bool)

 ok := check(x);
 if (ok)
   do /* последнее присваивание только текстуально,
         но не обязательно во времени, особенно в циклах */
     ok = nextDo(<>x, >last)
   while (~last);
// ok = true // ошибка, ok уже зафиксирована в цикле выше
 else
   // позволена, ведь фиксация ok была выше, но в другой ветке
   ok := tryOther(y) 
 end;
//ok = true // ошибка, даже если выполнилась else с обычным присваиванием
}

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

Подпрограммы

• Процедуры — наиболее общие подпрограммы. Могут содержать выходные параметры и побочные эффекты. Возвращаемое значение необязательно.
• Функции — ограниченные подпрограммы без внешних побочных эффектов с входными неизменяемыми параметрами и возвращаемым значением. Внутри себя могут содержать локальные побочные эффекты
  • Константные функции — тривиально вычислимые на этапе трансляции для константых параметров. Не содержат циклов и рекурсивных вызовов.

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

section example0 {
 const (
  infoSize = 4;
  
  //константные функции объявляются в разделе констант
  func optimalAllocSize(main, x0 int) (x1 int) {
    var (total, fixed int)
    
    fixed := main + infoSize;
    total := x0 + fixed;
    if (total <= 16)
      total := 16
    else
      total := -(-total) / 32 * 32
    end;
    x1 := total - fixed
  }
  
  //такие функции можно использовать для получения констант
  dataSize = optimalAllocSize(33, 22)
  
 )
 
 //эта функция содержит цикл и не может возвращать константы 
 func min(a []int) (val int) {
  var (i int)

  val := a[0];
  for (i = 1; i < len(a); i += 1)
    if (val > a[i])
      val := a[i]
    end
  end
 }

 // процедура с изменяемыми параметрами 
 proc swap(<>a, <>b int) {
  var (t int)
  t := a;
  a := b;
  b := t
 }
 
 proc test(a, b int) {
  var (c, d int)
  // константные функции можно использовать и для переменных
  c := optimalAllocSize(a, b);
  d := 1;
  swap(<>c, <>d)
 }
 
}.

Разновидности параметров

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

• По значению — без отметок.
• Ссылочный параметр. Обозначается знаками «<>». Используется для чтения и записи в произвольном порядке.
• Выходной параметр. Требует предшествующего знака «>». Перед чтением в самой процедуре требует предварительного присваивания. Если его не было, то после вызова процедуры значение параметра должно считаться неначализированным. Возможность отсутствия присваивания должна быть указана в объявлении, иначе это считается ошибкой.
• Ссылочный параметр только для чтения. Предназначен только для параметров структурного типа (массивов и записей) для избежания избыточного копирования и для обобщённого кода. Предваряется знаком «<», но не обязателен для открытых массивов, так как они в общенм случае и так не могут передаваться по значению.
• Закрываемый параметр. Обозначается буквой «Х»(необязательно «X>»). После вызова процедуры переменная-фактический параметр считается неначализированной.

section example1 {
 type ( file { i int } )
  
 proc open(>f file) {
  f.i := 0
 }
  
 proc read(<>f) (val int) {
  val := f.i;
  f.i += 1
 }
  
 proc close(Х f file) {
  // X f // подразумевается неопределённость в f
 }
  
 proc test {
  var ( f file; i int )
  //i := read(<>f);// ошибка трансляции
  open(>f);
  i := read(<>f);
  close(X f);
  // i := read(<>f); // ошибка трансляции
  open(>f)
 }
}.

Утверждения в подпрограммном типе. Пред- и пост- условия

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

section range {

 type ( +t { +@min, +@max int } )

 proc +init(>r t, mn, mx int)
 [ // предусловие
  ! mn <= mx
 post: // постусловие
  ! t.min = mn
  ! t.max = mx
 ]
 {
  t.min := mn;
  t.max := mx
 }

}.

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

Утверждения, которые верны и для пред-, и для пост- условий, можно не дублировать, а записать один раз после «inv:», находящегося между их секциями.

• Пред- и пост- условия состоят из утверждений, разрешений и ветвлений
• В каждом утверждении обязан присутствовать хотя бы один из параметров
• Из подпрограмм в выражениях утверждений могут использоваться только константные функции. Механизм предназначен для сравнительно легковесных проверок
• Выходные параметры «>» не могут присутствовать в предусловиях
• Закрываемые параметры «X» не могут присутствовать в постусловиях
• Нарушение утверждений в вызовах подпрограмм считается ошибочным состоянием, кроме случая явного учёта правильности
• Применение в утверждениях непрозрачных предикатов тоже считается ошибочным состоянием, хотя в общем случае и сложно диагностируемым

Проверка параметров

Предусловия можно использовать для проверки входных параметров с помощью механизма явного взятия правильности

section example2 {

 import ( range, log )
 
 var (a, b int)

 proc +test {
  var (r range:t; ok bool)

  /* мягко проверяются только утверждения, 
    куда входят параметры, помеченные «?» */
  ok ?? range:init(>r, ? a, b);
  log.b(ok);// false 
  
  ok ?? range:init(>r, ? b, ? a);
  log.b(ok);// true 
 }

 { a := 32; b := -23 }

}.

Разрешения

Если утверждения сужают область значений, то разрешения, наоборот, ослабляют некоторые требования по умолчанию, например, необходимость установки значений выходным параметрам

 proc example3(>out []int) (ok bool) [ 
 post:
  allow uninit (out)
 ] {
  var ( i int )
  ok := false;
  if (ok)
    for (i := 0; i < len(out); i += 1)
      out[i] := len(out) - i
    end
  end
 }

Разрешение на неначализированность выходного параметра после вызова процедуры позволено, если

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

Разрешение на неначализированность входного или ссылочного параметра после вызова процедуры позволено, если

1. есть входной или ссылочный параметр без возможности неначализированности

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

Для входных и ссылочных параметров есть разрешение на неиспользование — allow unuse name, что может быть необходимо для соблюдения сигнатуры, например, для совместимости.

Полнота требований

Наличие явных требований к параметрам в объявлении ещё не означает, что они полны, то есть не составлены по принципу «лучше, чем ничего». Для указания, что требования исчерпывающие следует использовать двойные прямоугольные скобки.

func add3(a, b int) (sum int) [[
 ! min(int) <= a + b <= max(int)
post:
 ! sum = a + b
]] {
 // переполнение невозможно при выполнении предусловий
 sum := a + b
}

Неявные требования и их отсутствие

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

func add1(a, b int) (sum int) {/* Законно предполагать, что add1 вызывается
   с параметрами, не вызывающими переполнение, но и гарантий этого нет */ 
 sum := a + b // поэтому нужен контроль во время выполнения
}

func add2(a, b int) (sum int) [[]] {
 // Здесь очевидно, что возможно переполнение, так как a и b — любые
 sum := a + b
}

Маршрутизация разделов

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

sections some {
  
  /* Необязательное перечисление имён как оглавление
  name ( ... ) 
  */

  // расположение доступных разделов
  locate (
    //простейшее указание по одному
    math = file("base/math.def");
    
    //группа разделов по маске через переменную name
    (path; io; sandbox/io; storage; random.pseudo; editor) 
      = file("base/"-name-".def");
    
    //файл может содержать несколько разделов
    (random; cypher) in file("base/cypher.defs") as section(name-".2");
    
    untrusted/editor := file("trash/editor.def");
    fileman := file("files/fileman.def");

    //заглушка для раздела
    compress := stub of file("base/compress.def")
  )
  
  // перечисляет ограниченные по умолчанию разделы 
  restricted = {path}
  
  /* указание доступности для импорта одних разделов другими.
    отсутствие прямого импорта не ограничивает косвенный импорт 
    и косвенные вызовы */
  allow (
    // редактор может получить доступ только к указанному файлу
    {path} for {editor}
    /* хранилище предоставляет ограниченный доступ к системе,
      но само имеет полный доступ для его воплощения */
    {path +all} for {storage}
    
    /* под видом предоставления некому недоверенному редактору 
      «полного» доступа к произвольным файлам даёт путь в изолированную
      песочницу, подменив раздел ввода-вывода */
    {path +all, io = sandbox/io} for {untrusted/editor}
    
    /* те разделы, что не указаны, видны всем (other for all)
      разделы с подразделами не могут входить в эту группу,
      так как подразделы и нужны для разграничения ответственности */
  )
  
  // отсутствие опциональных разделов
  disable (
    {compress} for {fileman}
  )
  
  // строгий запрет на прямое и косвенное использование разделов 
  deny (
    // настоящий ГПСЧ не должен использовать ввод 
    {io} for {random/pseudo}
  )

}

Строгий запрет на использование одних разделов другими подразумевает и довольно сложный запрет на прямой или косвенный вызов процедурных переменных (полиморфных объектов), находящихся в других разделах, так как это может привести к косвенному переносу запрещённого функционала. Возможно использование процедурных переменных, лежащих внутри самого раздела, но запрещено менять их за пределами места начализации переменных в этом разделе. Также возможно явное разрешение на вызов сторонних процедур через формальные параметры подпрограмм раздела. Без возможности менять внутренние переменные это не позволяет провести внедрение запрещённого функционала в сам раздел, а косвенное применение всё равно в конечном итоге производится из вызова, которому это разрешено.

Ошибочное состояние

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

Ближайшим аналогом из других языков является термин «неопределённое поведение»[0] с поправкой на правильно выставленный приоритет в отношении понимания и обработки.

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

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

Примеры операций, приводящих к ошибочному состоянию в случае отсутствия явного учёта состояния правильности:

• Арифметическое переполнение допустимого диапазона чисел — и целых, и дробей
• Деление на 0
• Обращение к массиву по индексу, выходящему за его пределы
• Чтение значения переменной с ошибочным значением (не- или де-начализированной)
• Преобразование типа для недопустимого значения
• Обращение по пустому указателю
• Обращение по недопустимому адресу в низкоуровневых операциях с данными
• Получение ложного значения в утверждении
• Достижение потоком выполнения места, помеченного как недостижимое
• Фактическое зацикливание

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

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

Примеры возможного воплощения поведения при ошибочном состоянии:

• Статическое выявление как ошибки компиляции для простых случаев или при продвинутом анализе. В отличий от опциональных предупреждений, которые могут быть ложно-положительными, диагностика ошибки допустима только для достоверных нарушений правил языка с учётом контекста применения. Поиск нарушений ведётся во все ветках кода, без учёта фактической достижимости.
• Аварийное завершение подзадачи в результате диагностики во время исполнения программы. Подходит для отладки и для быстрых проверок хорошо отлаженного кода в выпускной версии.
• Диагностика и пометка выходного значения как ошибочного. Другие вычисления с ошибочными значением тоже порождают ошибочное значение, возможно, кроме тех, что приводят к определённому значению вне зависимости от другого значения (e * 0, e & false). Если ошибочное значение добирается до существенной развилки или вывода данных, то происходит аварийное завершение. Если ошибочное значение оказывается незадействованным или уничтоженным, то программа может продолжить нормальное выполнение.
• Максимизация случайного поведения. Подходит для отладки того, что сложней диагностировать аварийной остановкой, например, работу с неинициализированными переменными. Гуляющее поведение свидетельствует об ошибках и препятствует закреплению случайных характеристик текущей версии исполнителя в ошибочном коде как чего-то ожидаемого[1].
• Максимизация детерминированности поведения, которое даёт наиболее вероятную правильность. Подходит для выпускной версии, но будет полезен только в паре с предыдущим. Если нужно выбрать что-то одно, лучше выбрать предыдущий.
• Приостановка выполнения и ожидание ответа пользователя, который может выбрать наиболее подходящее решения на основе анализа конкретной ситуации. Подходит для длительных задач личного характера.
• Предотвращение нарушений, но без аварийной остановки кода-нарушителя, а возвратом значения ошибки, то есть преобразования ошибки кода в специальное значение, например, ошибку ввода. Подходит для повышения устойчивости кода, менее критичного к последствиям ошибок кода, и в тех подзадачах, где допустимо некоторое значение по умолчанию.
• Отсутствие специальной реакции, как и необходимости обеспечения детерминированности. Такая возможность — это лишь признание сложности диагностики некоторых ошибок, например, зацикливания, но без требования отказа от их диагностики. Применимо не только к простым трансляторам, но и тем, что работают в связке с системами доказательства правильности, позволяющих, как минимум, доказать отсутствие в коде возможности достижения ошибочного состояния.

Сноски

[0] Не исключено, что неудачно выбранное название и привело к тому, что большинство разработчиков понимают эту тему неточно в той или иной степени.
[1] Противодействие закону Хирума. Именно этот закон приводит многих разработчиков к ошибочному выводу о том, что ошибочное состояние/неопределённое поведение является причиной дополнительных ошибок, ведь у них раньше работало.