Здесь хочется отметить некоторые сторонние языки программирования как из-за их схожести в постановке задач, так и из-за различия.
EctasyLang позиционируется как первый язык, спроектированный для облачных решений, но как по идеолоигии, так и по ряду конкретных решений напоминает формулируемый здесь язык защитного программирования.
Для лучшего достижения целей надёжного программирования транслятору языка необходимо обладать заданными свойствами, которые сложно совместить в единой программе, поэтому целесообразно заложить несколько различных трансляторов, совместно позволяющих добиться поставленных целей. Также можно добавить, что стандарты надёжного программирования для уменьшения вероятности внесённых инструментами ошибок могут требовать сборки программы тремя независимыми трансляторами.
Можно выделить 4-е основные свойства, задающие назначение инструмента:
Определяющий. Для избежания раночтений надёжному языку необходимо его чёткое определение. Пожалуй, самым чётким возможным определением, хотя бы и вспомогательным, является формальное описание. А полное формальное описание языка, хотя бы и гипотетически, позволяет получить из него пригодный для выполнения на машине исполнитель языка. Его целью является максимально понятное описания минимально размера, а не эффективность и удобство использования, поэтому кроме исключительных случаев такой транслятор не может использоваться разработчиком напрямую. Зато он может служить образцом для более сложных трансляторов и, в том числе, использоваться как часть тестовой системы или как формальная спецификация для транслятора с доказанной корректностью.
Юркий. Небольшой, простой и быстрый транслятор с минимальными внешними зависимостями бывает крайне полезен и позволяет расширить область применимости языка в качестве встраиваемого решения. Также может служить для самораскрутки проекта. Желательно предоставление исполнения кода непосредственно из исходных кодов.
Доказанный. Полное формальное доказательство корректности позволяет исключить из прагматичного транслятора ошибки относительно спецификации языка. Наличие такого транслятора можно считать обязательным для будущих проектов, требующих максимальной надёжности. Так как доказательство является сложной задачей, то для её облегчения или даже, вообще, возможности код транслятора нужно с самого начала писать под доказательство, выбирая для его воплощения такие решения, которые легче для доказательства, но могут отрицательно влиять на пользовательские качества. Поэтому такой транслятор не может совпадать с другими прагматическими трансляторами.
Многоцелевой. Это основной транслятор и он должен решать множество самых разных задач разработчика, во многом, связанных между собой:
В типичном сценарии программный код пишется итерационно — сначала создаётся первичная версия рабочего кода, затем она постепенно дорабатывается для улучшения поддержки заданных свойств. Хорошо спроектированный язык может способствовать этой важнейшей модели разработки, тем самым позволяя уменьшить издержки и позволяя добиться большей надёжности при сопоставимых затратах на разработку на менее удачных языках.
Это означает, что язык по возможности не должен заставлять переписывать дорабатываемые части кода, а способствовать их минимальному изменению. Особенно когда это касается доработки прямолинейного кода до верифицированного и надёжно защищённого от ошибок входных данных. Также, язык должен обладать свойствами, которые позволяют легче преобразовывать код под изменяющиеся условия — подробней.
Практически каждый программист является создателем языков программирования. Каждый раз когда разработчик задумывается о том, почему в используемом языке чего-то не хватает или, наоборот, что-то мешается, он создаёт в своей голове образ изменённого языка, лучше соответствующего его желаниям. Такие образы могут содержать как дельные рационализаторские предложения, так и быть смесью неупорядоченных, возможно, противоречивых возможностей, заимствованных из других языков или желаний. За воплощение таких языков большинство разработчиков никогда не возьмётся, но, тем менее, такие упражнения вполне можно назвать созданием языка. Поэтому размышления о возможных ошибках при проектировании языка в контексте достижения корректности кода могут быть интересными многим, также позволяя лучше понять те или иные вопросы дизайна языка.
В языке для написания критичного к ошибкам кода нужен особый подход к целочисленным типам, позволяющий уменьшить вероятность переполнения, а потому способствующий корректности программ.
Целочисленные типы должны быть разделены на две группы:Разделение сделает более удобным, а потому и более желанным использование типов, для которых риск совершения ошибки ниже, оставив возможность использовать более редкие особые случаи, которые будут применяться только в тех задачах, где они нужны.
| Название | Диапазон допустимых значений |
|---|---|
| byte | 0 .. (28 - 1) |
| int | -(231 - 1) .. (231 - 1) |
| longint | -(263 - 1) .. (263 - 1) |
Тип byte как особая разновидность целочисленных типов нужен в первую очередь для обработки блоков данных, например, для чтения и записи в файлы. Поэтому это единственный встроенный беззнаковый целочисленный тип, так как знаковость в таких задач только мешает. В арифметических операциях и при передаче в качестве фактического параметра-значения в вызове функции он эквивалентен типу int. Остальные же беззнаковые типы не включены в предопределение из-за того, что близость нижней границы повышает вероятность переполнения, и необходимость согласования знаковых и беззнаковых целых приводит к дополнительному источнику ошибок.
int и longint - знаковые, симметричные относительно 0 типы. Равенство по модулю максимального и минимального значений упрощает учёт корректных вычислений, в частности, гарантирует, что смена знака и значение по модулю всегда выполнимы без переполнения. Это важней желания вместить на одно допустимое значение больше, как это позволяют наиболее распространённые ныне платформы из-за использования дополнительного кода для кодирования отрицательных чисел. В большинстве случаев минимальное отрицательное даже не нужно, но непропорционально своему значению требует избыточного внимания в случае необходимости достижения полной корректности.
Главным целочисленным типом является int, так как он представляет хороший компромисс по предоставляемому диапазону чисел, достаточного для большинства задач, и возможностью эффективной обработки. В частности, количество элементов массива не может превышать максимального значения int. longint нужен как из-за того, что в современных условиях нередки ситуации, где диапазона 32-битных значений всё же не хватает, например, для кодирования времени в наносекундах или обработки больших файлов, так и потому что расширенный диапазон естественным образом возникает при вычислениях в полном диапазоне int.
Остальные целочисленные типы других диапазонов вынесены из ядра языка, так как потребность в них ниже основных, что, однако, не препятствует нередкому злоупотреблению ними и может приводить к лишней потребности сопряжения целочисленных типов разных диапазонов, что, в свою очередь, служит дополнительным источником ошибок.
В арифметических выражениях, в которых смешиваются операнды разных целочисленных типов, операнды меньшего типа рассматриваются как эквивалентные операнды наибольшего. Вычисления выражений для операндов в byte неявно происходят в диапазоне int, для int и longint в диапазоне longint. Контроль переполнения происходит как в выражениях, так и при сохранении значения. Если диапазон приёмника меньше диапазона типа выражения, требуется явное преобразование типа. Если такой же или больше, то не требуется, но контроль переполнения выполняется в любом случае. Такое правило позволяет уменьшить вероятность переполнений и не требует избыточных явных приведений типа.
Например, следующие операции, которые во многих других языках могут содержать ошибки переполнения при определённых значениях переменных, в защитном языке оказываются всегда корректны:
| Защитный язык | Java |
|---|---|
var (a, b, c int; d longint; f bool) a = max(int) / 2; b = a + 2; c = 300; f = a + b < c; // false d = a * b; // 1152921504606846975 c = b * 2 / 3 // 715827883 |
int a, b, c; long d; boolean f; a = Integer.MAX_VALUE / 2; b = a + 2; c = 300; f = a + b < c; // true d = a * b; // -1 c = b * 2 / 3; // -715827882 |
Вторую группу целочисленных типов должны представить типы из состава специальных разделов, отличающихся знаковостью и разрядностью гарантированных диапазонов. Разделы должны предоставлять почти одинаковые наборы функций для работы с собственными целочисленными типами. Имена разделов можно вывести из синтаксического уравнения - имя = [u]int(8|16|32|64), где u обозначает беззнаковость, а число, естественно - разрядность типа. Диапазоны допустимых значений определяются по формулам - [0 .. 2n-1] для беззнаковых и [-2n-1 .. 2n-1-1] для чисел со знаком, так как они должны быть закодированы через двоичное дополнение.
type (t) // сам целочисленный тип
var (min, max t) // минимальное и максимальное значение
// Группа функций, которые трактуют переполнение как ошибку.
// Если при их выполнении не было явно получено состояние корректности,
// то в случае переполнения они завершают выполнение программы.
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);
// Функции интерпретации стандартных типов как соответствующих их
// диапазону типов из разделов противоположной знаковости и наоборот.
// в разделе int8:
func as_byte(value t) (result byte);
func as_t(value byte) (result t);
// в разделе uint32:
func as_int(value t) (result int);
func as_t(value int) (result t);
// в разделе uint64:
func as_longint(value t) (result longint);
func as_t(value longint) (result t);
Битовые операции для встроенных целочисленных типов не предусмотрены как неуместные. Вместо них вводятся:
func pow(v, n int) (res int) или отдельная операция
v^n. Выбор будет сделан позднее.Дополнительные материалы:
В программировании часто возникает задача проверки корректности входных данных, которые могут привести к одному из нежелательных последствий, вроде арифметического переполнения, выход за границы массива и других. Особенно остро стоит проблема для задач, связанных с безопасностью, так как через подачу неправильных данных можно добиться непредусмотренного поведения. Явная проверка корректности нередко требует действий, сопоставимых по объёму с основными действиями. Это приводит к частому игнорированию проверок или их некорректному составлению, что также плохо выявляется тестированием, так как каждые по отдельности случаи некорректных данных, как правило, встречаются реже корректных.
Необходим механизм, который позволит сделать проверки синтаксически более легковесными. Для языка защищённого программирования таковым становится явно выведенное состояние корректности.
Многие языки программирования используют явное понятие некорректности, известное как механизм исключений, но такой вид неприемлем для наших целей. Исключения сами порождают проблемы, например, они часто смешивают ошибки входных данных с ошибками в самой программе, а также, они нарушают принцип структурного программирования, что является важной составляющей проектируемого языка. Поэтому в новом языке понятие корректности будет выведено иным способом.
Рассмотрим для примера сложение — так выглядит оно без явных проверок:
sum = a1 + a2;
При переполнении такая программа должна аварийно завершиться. Чтобы проверить возможность переполнения и выполнить сложение только при его отсутствии, можно было бы использовать явные проверки:
if (a2 >= 0)
correct = a1 <= max(int) - a2
else
correct = a1 >= min(int) - a2
end;
if (correct)
sum = a1 + a2
end
Или, при наличии специальной функции, такого кода:
correct = add(> sum, a1, a2);
Язык предлагает такую запись для выполнения действия и явного получения его корректности:
correct ?= sum = a1 +? a2;
Лексема «?=» служит для обозначения присваивания состояния корректности, а «?» придаёт операции возможность передать это состояние в соответствующую логическую переменную. Без этого знака поведение операции будет обычным несмотря на наличие «?=».
Использование «?» для пометки операций с проверками вместо того, чтобы придать проверочных свойств всем действиям в выражении нужно для того, чтобы не злоупотреблять этим свойством и проверять только те операции, что нужно, отделяя обработку ошибок входных данных от ошибок в самой программе.
Необходимость же введения специальных знаков вместо использования функций, вроде указанной add, объясняется на более сложных примерах. Незащищенный проверками код:
a = b[i] * b[0] + c;
Код с проверками на функциях:
correct = (i >= 0) & (i < len(b)) & mul(> m, b[i], b[0]) & add(> a, m, c);
Новый подход:
correct ?= a = b[?i] *? b[0] +? c;
Этот способ лучше читается и позволяет обойтись без переписывания первоначального кода, обеспечивая непрерывность в его сопровождении — сначала можно написать незащищённый прототип, а затем небольшими правками защитить его от некорректных данных. Небольшие правки позволяют избежать ошибок переписывания.
Действия, для которых доступна проверка с помощью «?»:
+?», «-?», «*?», «/?», «%?»+?=», «-?=», «*?=», «/?=», «%?=»array[? i], matrix[? y][? x]new(param)?pstr .? itemfun(param)?fun(? param) recursive(? deep) fun(param) int(? rational)base.(? extended)В этом вопросе язык для надёжного программирования ближе всего к Оберону, но с более жёсткими условиями по недопущению перекрытия.
Все используемые идентификаторы кроме предопределённых должны быть предварительно объявлены. Имя, использованное для объявления на уровне модуля или функции, должно быть уникальным в одной области видимости, за исключением предварительного объявления функции, что нужно для возможности косвенной рекурсии. Имя объявления, сделанного внутри функции также должно быть уникальным во всей функции, в том числе и для не пересекающихся областей видимости внутри неё.
Объявление-d, сделанное на уровне модуля-m доступно по имени от начала его появления в тексте до конца m. В других модулях-am d доступно только в том случае, если оно было помечено как экспортируемое в m, и только в тех из них, где m был импортирован. Доступ к d в am осуществляется через импортированное имя m - im, следующей за ним разделяющей точкой и именем d
module m {
const(c = d + 1; // ошибка - d ещё не объявлена
+d = 0; // пометка объявления "+" как экспортированное
e = d + 1)
proc p() {
const(f = d;
e = 6) // ошибка - е уже объявлено в этой области уровнем выше
...
}
}
module am {
import(im = m) // переименовываем, m недоступна для использования
const(d = im.d;
e = m.d; // ошибка, модуль m был переименован для использования
f = im.e) // ошибка, объявление е не было экспортировано в m
proc p() {
{ const (a = 3)
...
}
{ const (a = 0.6)// ошибка - хотя a=0.6 объявлена в другой области
... // видимости, но в пределах одной процедуры,
} // что запрещено
}
}
Имя объявления, сделанного на уровне структуры должно быть уникальным лишь
в пределах самой структуры. Имя может совпадать как с предопределёнными
именами, так и с именами, объявленными на уровне модуля, функций и других
структур, в том числе вложенных, так как из-за строго иерархического обращения
к элементам структуры не может быть никакого кофликта имён.
module a {
const (b = 1)
var (r struct {
r struct {
r, b int
}
}
)
proc p() {
r.r.r = 0;
r.r.b = 1
}
}
В языке нет разновидности импорта, позволяющей включать экспортированные объявления других модулей в область видимость импортирующего модуля так, как будто они являются его собственными. Это сомнительное удобство вносит неразбириху относительно принадлежности используемых сущностей и создаёт возможность для появления ошибок в результате манипуляций с импортом и расширения интерфейса используемых модулей.
Из заданных ограничений следует, что имена объявлений, сделанные внутри функции могут совпадать с именами объявлений, сделанных в других функциях. Также, имя внутри функции может совпадать с именем одной из функций, объявленных ниже по тексту. Это послабление нужно для возможности создания однопроходного транслятора.
module a {
const(+a = 10)// обращение к собственному модулю не предусмотрено,
// поэтому имя объявления может совпадать с именем модуля.
proc +b() {
const(c = a;
d = 4)// d объявлена ниже, поэтому не входит в текущую
... // область видимости
}
proc +d() { // область видимости d = 4 закончилась внутри b()
const(c = a + 1)// хотя с уже встречается в b(), но так как области
// b() и d() не пересекаются, то объявление корректно.
...
}
}
Запрет на перекрытие имён и возможность иметь несколько конкретизаций синтаксисов создают
трудности, требующие разрешения:
module @const { // @ как в C#
const (+@module = 1)
}
Я рассматриваю и другую возможность - отказ от ключевых слов и ограниченное число предопределённых имён. При необходимости добавления новых в обновлённой версии языка, они добавляются в псевдомодуль, чтобы исключить пересечение с именами в модуле, написанном ранее. Но это решение пока кажется сложней и проблематичней. Вариант, в котором наоборот - все ключевые слова и предопределённые идентификаторы помечены, кажется мне слишком неудобным и уродливым.
@module m {
@const (c = 1)
@type (t @int)
@var (v t)
@func f(i t) (res @bool) {
res = i < @max(t) / 2
}
}
Организующей программной единицей является раздел. В ряде языков их называют модулями [0].
section name {
/* Это именованное место для упорядоченных объявлений:
типов, констант, переменных, функций. */
}.
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 (
d.m; /* в качестве идентификатора раздела после импорта */
d.m2; /* используется только вторая часть имени после точки */
bm = b.m/* переименование, чтобы избежать ошибки совпадения имён */
)
const (c4 = m.c1 + m2.c2 + bm.c3)
}.
Для удобства разграничения возможностей, предоставляемых импортирующим разделам, раздел может быть разбит на части, ограниченно владеющие функционалом. Необходимо лучше продумать синтаксис разделения, но как пример оно может выглядеть так:
section path+content+full {
type (+t)
section content+full {
type (
+t = {
+name string;
+next *t
}
)
section full {
proc +new(name string, subpath *t) (path *t) { ... }
} full;
} content+full;
} path+content+full.
section editor {
import (
/* path+full; */ /* после импорта должен быть доступен по имени path,
но если у editor нет доступа к полному разделу,
то здесь была бы ошибка трансляции */
path /* эта часть позволяет получать доступ к ресурсам, пути к
которым явно переданы параметрами, но не позволяет
самостоятельно указывать, с какими ресурсами можно работать,
как и не даёт доступа к самому имени */
)
proc +do(file path:t) { ... }
}.
По сравнению с некоторыми другими способами обособления такое разделение позволяет легче доказывать отсутствие в меньших интерфейсах предоставления лишних возможностей. Нет смешивания, в которм было бы легко потерять включение чего-то ненужного. Чего нет в подразделе, то точно недоступно. Вынесение разделения на пользовательский уровень вместе с другими мерами позволит получить гарантии отсутствия нежелательного доступа у произвольного исполнимого кода уже на этапе верификации кода, что даст гораздо лучшую предсказумость и понятность системы в сравнении с устаревшим подходом.
При трансляции корректного раздела может создаваться два файла: один с исполнимым кодом, другой - интерфейсный для возможности независимой сборки импортирующих его разделов. Лучше, если исполнимый код будет не специфичным для машины, хотя и с возможностью внедрения машинного кода, выступающего как оптимизированная альтернатива основному коду. Для обоих файлов должны быть предусмотрены контроль целостности и подпись.
Чтобы избежать случайного изменения интерфейса раздела, транслятор по умолчанию должен выдавать ошибку, если вновь созданный интерфейсный файл не совпадает с предыдущим. В инструментарии для больших команд следует предусмотреть возможность распределения ролей, в которых некоторым разработчикам запрещается менять интерфейс целевых, не вспомогательных разделов, над которыми они работают.
В операционных системах, где были бы воплощены идеи хотя бы 80-х, а не мусолились идеи 60-70-х, раздел может служить главной и единственной единицей загрузки вместо россыпи таких понятий как программа, статическая и динамическая библиотеки. В морально устаревших же операционных системах нужно будет выполнить наподобие этого:
$ sc build util.do
Что приведёт к созданию исполнимого файла util, полученного из одноименного раздела с точкой входа do - экспортированной процедуры без параметров.
Чтобы понять почему так, нужно ответить на вопрос: Если ответ - «не должен», значит, истинными модулями являются отдельные объявления раздела, а не сам раздел. Объявления пронизаны неявным импортом внутренних объявлений, необходимого для избежания чрезмерного перечисления используемых связей, что было бы нужно в случае раздельного оформления отдельных сущностей раздела.
Дополнительные сведения:
[1]
Оберон умер, да здравствует Оберон! Часть 2. Модули[0]Почему раздел - это не модуль или unit?
«Если в разделе несовместимо изменилось экспортированное объявление, должен ли он потерять совместимость с разделами, использующими другие его неизменившиеся объявления?»
[2]
Михаэль Франц Динамическая кодогенерация: ключ к разработке переносимого
программного обеспечения
[3]
Webassembly: Design Rationale