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

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 ( math, path, io, sandbox/io, storage, random.pseudo, editor, 
         random, cypher, untrusted/editor, fileman, compress)
  */

  // расположение доступных разделов
  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] Противодействие закону Хирума. Именно этот закон приводит многих разработчиков к ошибочному выводу о том, что ошибочное состояние/неопределённое поведение является причиной дополнительных ошибок, ведь у них раньше работало, что достигалось ненадёжным подходом правки кода, пока не заработает, вместо устранения всех потенциально выявляемых ошибок.

Целочисленные типы

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

Целочисленные типы должны быть разделены на две группы:

1. Ограниченное число предопределённых типов, подходящих для большинства задач, и к которым применимы встроенные арифметические операции: +, -, *, /, %.
2. Типы из разделов, для работы с которыми необходимо использовать функции из тех же разделов с соответствующими названиями: add, sub, mul, div, mod и т.д.

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

Предопределённые типы

В первую группу должны войти:

Название	Отрезок допустимых значений
int	-(231 - 1) .. (231 - 1)
longint	-(263 - 2) .. (263 - 2)

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

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

byte занимает особое место — он нужен в первую очередь как строительный элемент, и сам по себе не является целочисленным типом, но легко может быть приведён к нему, равно как и в обратном направлении. byte соответствует отрезку значений 0 .. 28 - 1.

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

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

***

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

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

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

Защитный язык	Java
var (a,b,c,m int; d longint; f bool) a = max(int) / 2; b = a + 2; c = 300; m = min(int); f = a + b < c; // false d = a * b; // 1152921504606846975 c = b * 2 / 3; // 715827883 m = -m; // 2147483647	int a, b, c, m; long d; boolean f; a = Integer.MAX_VALUE / 2; b = a + 2; c = 300; m = Integer.MIN_VALUE; f = a + b < c; // true d = a * b; // -1 c = b * 2 / 3; // -715827882 m = -m; //-2147483648

Типы предопределённых разделов

Вторую группу целочисленных типов должны представить типы из состава специальных разделов, отличающихся знаковостью и разрядностью гарантированных диапазонов. Разделы должны предоставлять почти одинаковые наборы функций для работы с собственными целочисленными типами. Имена разделов можно вывести из синтаксического уравнения – имя = [u]int(8|16|32|64), где u обозначает беззнаковость, а число, естественно — разрядность типа. Диапазоны допустимых значений определяются по формулам - [0 .. 2n-1] для беззнаковых и [-2n-1 .. 2n-1-1] для чисел со знаком, так как они должны быть закодированы через двоичное дополнение.

Объявления разделов:

type (t) // сам целочисленный тип

const (min, max) // минимальное и максимальное значение

// Группа функций, которые трактуют переполнение как ошибку.
// Если при их выполнении не было явно получено состояние правильности,
// то в случае переполнения они завершают выполнение программы.
func add(addend1,  addend2 t)    (sum t);
func sub(minuend,  subtrahend t) (difference t);
func mul(factor1,  factor2 t)    (product t);
func div(divident, divisor t)    (ratio t);
func mod(divident, divisor t)    (remainder t);

// Группа процедур, для которых переполнение сопровождается воображаемым
// отбросом старших разрядов.
proc mod_add(addend1, addend2,    > sum t)        (overflow bool);
proc mod_sub(minuend, subtrahend, > difference t) (overflow bool);
proc mod_mul(factor1, factor2,    > product t)    (overflow bool);

// Функции для преобразования к основным типам и обратно. Поскольку при
// этом может возникнуть переполнение, то функции также подразумевают
// явное взятие правильности, либо завершение работы.
func to_byte   (value? t) (result byte);
func to_int    (value? t) (result int);
func to_longint(value? t) (result longint);

func from_byte   (value byte)    (result t);
func from_int    (value int)     (result t);
func from_longint(value longint) (result t);

// Функции интерпретации стандартных типов как соответствующих их
// диапазону типов из разделов противоположной знаковости и наоборот.

// в разделе uint64:
func as_int64  (value t) (result int64.t);
func as_longint(value t) (result longint);
func as_t(value longint) (result t);

// в разделе uint32:
func as_int32  (value t) (result int32.t);
func as_int    (value t) (result int);
func as_longint(value t) (result longint);
func as_t    (value int) (result t);

// в разделе int8:
func as_byte   (value t) (result byte);
func as_int    (value t) (result int);
func as_longint(value t) (result longint);
func as_t   (value byte) (result t);

Битовые операции для встроенных целочисленных типов не предусмотрены как неуместные. Вместо них вводятся:

1. Встроенная функция для возведения в степень func pow(v, n int) (res longint) или отдельная операция v**n. Выбор будет сделан позднее.
2. Типы-множества, которые можно приводить к целочисленным и обратно и о которых подробней будет рассказано в отдельной заметке.

Дополнительные материалы:

1. Danger – unsigned types used here!
2. INT14-C. Avoid performing bitwise and arithmetic operations on the same data.

Состояние правильности

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

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

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

Рассмотрим для примера сложение — так выглядит оно без явных проверок:

sum = a1 + a2;

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

if (a2 >= 0) 
    ok = a1 <= max(int) - a2
else
    ok = a1 >= min(int) - a2
end;
if (ok)
    sum = a1 + a2
end

Или, при наличии специальной функции, такого кода:

ok = add(> sum, a1, a2);

Язык предлагает такую запись для выполнения действия и явного получения его правильности:

ok ?? sum = a1 +? a2;

Лексема «??» служит для обозначения присваивания состояния правильности, а «?» придаёт операции возможность передать это состояние в соответствующую логическую переменную. Без этого знака поведение операции будет обычным несмотря на наличие «??».

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

Необходимость же введения специальных знаков вместо использования функций, вроде указанной add, объясняется на более сложных примерах. Незащищенный проверками код:

a = b[i] * b[0] + c;

Код с проверками на функциях:

ok = (i >= 0) & (i < len(b)) & mul(> m, b[i], b[0]) & add(> a, m, c);

Новый подход:

ok ??  a = b[?i] *? b[0] +? c;

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

Действия, для которых доступна проверка с помощью «?»:

1. Арифметика: «+?», «-?», «*?», «/?», «%?»
2. Арифметика совместно с присваиванием: «+?=», «-?=», «*?=», «/?=», «%?=»
3. Обращение к элементу массива: array[? i], matrix[? y][? x]
4. Выделение динамической памяти тоже можно сделать с показателем правильности для избежания лишних проверок на null: new(param)?
5. Обращение к элементу структуры, заданной указателем, который может быть пустым: pstr .? item
6. Вызов функции, которая может возвращать состояние неправильности: fun(param)?
7. Вызов функции с проверкой правильности параметра: fun(? param)
8. Вызов рекурсивной функции при исчерпании допустимой глубины вызовов recursive(? deep) fun(param)
9. Преобразование типа: int(? rational)
10. Уточнение динамического типа — переход от основы к расширению (от предка к наследнику): base.(? extended)

Объявления и области видимости

В этом вопросе язык для надёжного программирования ближе всего к Оберону.

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

Объявление-d, сделанное на уровне раздела-s доступно по имени от начала его появления в тексте до конца s. В других разделах-so d доступно только в том случае, если оно было помечено как экспортируемое в s, и только в тех из них, где s был импортирован. Доступ к d в so осуществляется черезимпортированное имя s - ins, следующей за ним разделяющей точкой и именем d

section s {
  const(c = d + 1; // ошибка - d ещё не объявлена
       +d = 0;     // пометка объявления "+" как экспортированное
        e = d + 1)
  
  proc p() {
    const(f = d;
          e = 6) // ошибка - е уже объявлено в этой области уровнем выше
    ...
  }
}.

section so {
  import (ins = so) // переименовываем, s недоступна для использования
  const (d = ins.d;
         e = so.d;  // ошибка, раздел s был переименован для использования
         f = ins.e) // ошибка, объявление е не было экспортировано в s
  
  proc p() {
    { const (a = 3)
      ...
    }
    { const (a = 0.6)// ошибка - хотя a=0.6 объявлена в другой области
      ...            // видимости, но в пределах одной процедуры,
    }                // что запрещено
  }
}.

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

section a {
  const (b = 1)
  var (r struct {
           r struct {
              r, b int
           }
         }
      )
  proc p() {
    r.r.r = 0;
    r.r.b = b
  }
}

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

Из заданных ограничений следует, что имена объявлений, сделанные внутри функции могут совпадать с именами объявлений, сделанных в других функциях. Также, имя внутри функции может совпадать с именем одной из функций, объявленных ниже по тексту. Это послабление нужно для возможности создания однопроходного транслятора.

section a {
  const(+a = 10)// обращение к собственному модулю не предусмотрено, 
                // поэтому имя объявления может совпадать с именем модуля.
  proc +b() {
    const(c = a;
          d = 4)// d объявлена ниже, поэтому не входит в текущую 
    ...         // область видимости
  }
  
  proc +d() { // область видимости d = 4 закончилась внутри b()
    const(c = a + 1)// хотя с уже встречается в b(), но так как области 
                    // b() и d() не пересекаются, то объявление правильно. 
    ...
  }
}

Запрет на перекрытие имён и возможность иметь несколько конкретизаций синтаксисов создают трудности, требующие разрешения:

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

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

section @const { // @ как в C#
  const (+@section = 1)
}

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

@section m {
  @const (c = 1)
  @type  (t @int)
  @var   (v t)
  
  @func f(i t) (res @bool) {
     res = i < @max(t) / 2
  }
}

Разделяемость (модульность)

Организующей программной единицей является раздел. В ряде языков, например, в Oberon их называют модулями [0].

section name {
 /* Это место перечисления используемых разделов 
    и упорядоченных объявлений в строгом порядке:
    констант, типов, переменных, функций,
    отдела начализации переменных */
}.

Oberon

MODULE name;
 (* Это место перечисления используемых разделов 
    и упорядоченных объявлений в строгом порядке:
    констант, типов, переменных, функций,
    отдела начализации переменных *)
END name.

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

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

section m1 {
  const (+a = 0;/* экспорт обозначен «+» перед именем */
          b = a + 1)
  ...
}.

section m2 {
  import (m1) /* доступ к элементам раздела через двоеточие */
  const (a = m1:a;/* a = 0 */
         b = m1:b)/* ошибка - константа "b" не экспортирована в "m1" */
  ...
}.

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

section m1 { import (m2) }.

section m2 {
  import (m1)/* ошибка - m1 уже ссылается на m2 */
}.

Назначение разделов

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

• Раздел может использоваться исключительно как вспомогательный, не влияя на интерфейс импортирующего раздела. Использование такого раздела может быть заменёно другим кодом, выполняющим те же задачи.
• Раздел, являющийся частью интерфейса импортирующего его раздела. Объявленные в нём типы могут становиться видимой частью экспортируемых объявлений импортирующего.
• Обобщённый раздел-заготовка, чьё определение задаётся не только его непосредственным содержимым, но также и импортированными разделами-параметрами.
• Опциональные разделы, наличие которых можно проверить в коде. Могут использоваться либо для создания более ограниченной версии раздела, либо для задействования более эффективных средств, не приводя к жёсткой зависимости от них.
• Декоративные разделы, служащие для удобства использования. Они каким-либо образом перестраивают взаимодействие с основным функционалом, практически не меняя его основной сути, например, объединяя интерфейсы разных разделов.

Поскольку разделов, особенно с учётом сторонних библиотек, может быть много, то возникает необходимость в создании иерархий:

section a/m  { const (+c1 = 1) }.
section a/m2 { const (+c2 = 2) }.
section b/m  { const (+c3 = 3) }.

section m {
  import (
    a/m;  /* в качестве идентификатора раздела после импорта     */
    a/m2; /* используется только вторая часть имени после точки */
    bm = b/m/* переименование, чтобы избежать ошибки совпадения имён */
  )
  const (c4 = m:c1 + m2:c2 + bm:c3)
}.

Версии разделов

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

В примере версии разделов указаны напрямую, но также их можно задать в проекте маршрутизации разделов[1], продолжая оперировать только именами в коде самих разделов.

section lib.0.1 { ... }
section lib.0.2 { ... }

section a { import (lib.0.1) }
section b { import (lib.0.2) }

section u { import (a; b; lib1 = lib.0.1; lib2 = lib.0.2) }

Разграничение, подразделы

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

/* path — это имя раздела, а name, clear и all — имена подразделов, 
  открывающие дополнительный функционал пользователям path, 
  которым дан доступ к этим подразделам и если 
  они их указывают при импорте */
section path +name+clear+all {

  type (+t) /* можно обозначить, не раскрывая содержимое */

section +name+clear+all:

  type (+t = { +name string })

section +clear+all:

  type (+t = { +up (*)t })

section +all:
  /* Только в этом подразделе позволено задавать путь, и без доступа 
    к нему путь к произвольным ресурсам закрыт по определению */
  proc +new(name string, indir (*)t) (path *t) { ...;
    path.name = name; path.up = indir }
  proc +str(spath string) (path *t) { ... }

} path.

section editor {
  import (
    /* path+all; */ /* после импорта должен быть доступен по имени path, 
                        но у editor нет доступа к полному разделу, 
                       и здесь была бы ошибка трансляции */

    path; /* эта часть позволяет получать доступ к ресурсам, пути к
            которым явно переданы параметрами, но не позволяет 
            самостоятельно указывать, с какими ресурсами можно работать, 
            как и не даёт доступа к самому имени */
    io 
  )
  proc +do(file path:t) {
    ... io.open(file)
    ...
    // io.open(path.str("~/.ssh/id_rsa")) // ошибка трансляции
  }
}.

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

• Добавление объявлений, включая элементы в ранее объявленные типы.
• Добавление экспортированности ранее закрытым объявлениям, включая отдельные элементы.

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

Трансляция

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

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

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

$ sc build util.do

Что приведёт к созданию исполнимого файла util, полученного из одноименного раздела с точкой входа do — экспортированной процедуры без параметров.

Сноски:

[0] Почему раздел — это не модуль/unit?

Необходимо ответить на вопрос: «Если в разделе несовместимо изменилось экспортированное объявление, должна ли потеряться совместимость с разделами, использующими только неизменившиеся его объявления?»

Если ответ — «не должен», значит истинными модулями являются отдельные объявления раздела, а не сам раздел. Раздел же служит организационной цели, так как отдельные объявления слишком мелки для этого. Объявления пронизаны неявным импортом других объявлений раздела для избежания чрезмерного перечисления используемых связей, что было бы нужно в случае раздельного их оформления.

[1] Маршрутизация разделов в защитном языке.
[2] Оберон умер, да здравствует Оберон! Часть 2. Модули
[3] Михаэль Франц Динамическая кодогенерация: ключ к разработке переносимого программного обеспечения
[4] Webassembly: Design Rationale

Синтаксис

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

Язык не обязан иметь лишь одну терминальную часть синтаксиса, которая отвечает за условную кодировку программы - вполне возможна такое воплощение средств программирования, которое позволяло бы конкретные детали синтаксиса выбирать по усмотрению разработчика, оставляя неизменной лишь ту центральную часть, которая ответственна за определения конструкций языка. Хотите C-подобный вид программ — пожалуйста. Больше по вкусу паскалевский подход — и это без проблем. Нужны ключевые слова на родном языке для обучения — и это возможно. Более того, исходный код не обязан быть представлен в виде традиционного печатного формата, а может использовать более богатое полиграфическое представление, а также и не обязан вообще иметь строковое представление, а быть оформленным, к примеру, в виде диаграмм. В развитых средствах программирования возможен учёт особых потребностей людей с инвалидностью, например, слепых или страдающих ДЦП.

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

Необходимость угодить среднестатистическому кодировщику не оставляет выбора — основная лексика должна быть Би-подобный как ныне наиболее популярная. Именно в языке B Кен Томпсон заложил основы вида кодировки, которая сейчас известна благодаря С.

Обсуждение хороших свойств некоторых языков в половине случаев застревает в обсуждении чего-то подобного begin и end, поэтому можно просто дать программистам их любимые {}, и вместо ненужных споров сосредоточиться на главном. Единственное, что нужно сделать, учитывая особенности Си — это привести его синтаксис к более понятному и ошибкоустойчивому виду, наподобие того, как это получилось у создателей Go. Собственно, ради экономии энергии в первом приближении можно взять синтаксис Go за основу, но без трепетного отношения ко всем его решениям, так как иная семантика связана с иным синтаксисом.

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