Средство обработки унифицированных по назначению данных (Sound – system for operating with unified data) разрабатывается для внятного программирования, обеспечивающего соответствие результатов вычислений назначениям. Под назначением данных понимается формальная спецификация вычислений, приводящих к этим данным. Язык программирования Sound нужен как универсальный инструмент, позволяющий транслировать вычислительную логику в любой язык программирования.
Внятное программирование подразумевает, что результат оценки выражения будет оставаться в рамках типа результата вычислений и соответствовать формальной спецификации. Таким образом, внятный язык программирования должен предоставлять инструменты прямого или косвенного ввода спецификации вместе с контролем корректности данных.
Назначение данных – это их логическое содержание, выраженное в качестве логической формулы, обозначающей смысл данных. Язык Sound позволяет косвенно выразить логические взаимосвязи между назначениями результатов промежуточных вычислений. Притом, что спецификация обычно вводится в комментариях к программе и на языке программирования не выражается, конструкции языка должны способствовать пониманию внутренней логики вычислений, чтобы читатель мог по возможности проверить соответствие этой логики требуемому результату.
Например, процедура преобразования числа в массив цифр состоит из зацикленного блока, принимающего на вход число и возвращающего его младшую цифру, которая затем сохраняется в очередной элемент последовательности. На языке Sound это выражается так:
from Compute where {DigitsRange=range(0), Sequence=Array<DigitsRange>, Number=Int} call NumberToDigits(100, 2)
module Compute:
type Sequence, DigitsRange, Number
func NumberToDigits (x: Number, base: Number) -> a: Sequence[DigitsRange] =
{
if x < 0:
Error.NegativeNumber(x)
k: DigitsRange = 0 # количество цифр
y = x # тип назначается автоматически
for:
next_digit(@y, base, @a, k) -> ok: Bool =
{
digit = lowest_digit (y, base) -> d: Number =
{
d = y % base
}
@a[k] = digit
@y /= base
ok = (y != 0)
}
if ok:
k += 1
else:
stop
if k == 0:
k = 1
a[0] = 0
}
Важным моментом в языках программирования являются имена, обозначающие те или иные понятия. В языке Sound есть три типа имен: 1) имена, обозначающие непосредственно данные того или иного типа; 2) имена, обозначающие конкретные типы данных; 3) имена, обозначающие абстрактные типы данных.
В Sound абстрактный тип данных – это имя, на место которого можно подставить имя любого конкретного типа данных, для которого логика вычислений не запрещает это сделать.
Пример абстрактного типа данных – индексируемый контейнер. Индексация производится с помощью типа «диапазон». В случае фиксированного числа индексов они перечисляются через запятую и берутся в квадратные скобки, в случае переменного числа индексов вводится тип «многомерный диапазон», который берется в двойные квадратные скобки. В качестве диапазона может выступать тип номеров индексов, специфичных для конкретного контейнера. Это означает, что язык может запретить индексировать с помощью одного и того же диапазона, скажем, числовую и строковую последовательности, потому что смысл индексов может различаться. Это может оказаться удобным в случаях, когда приходится работать сразу со многими данными, и каждая переменная-индекс обозначает обращение к данным определенного типа.
Унификация назначения данных означает, что с каждым именем, обозначающим данные, определяется семантика хранимых данных. В примере с переводом числа в последовательность цифр эта семантика выражена в именованном блоке.
Однако хотелось бы иметь возможность выразить на языке логические взаимосвязи между вычислительными блоками, чтобы, читая программу, можно было решить, соответствует ли логика вычислений назначениям. Язык унификации назначения данных включает в себя следующие элементы:
внешние интерфейсы – модели данных
внутренние интерфейсы – структуры данных
назначения – семантика данных
В рассмотренном примере в качестве назначения данных выступает повторение блока с переходом из состояния с номером k в состояние с номером k+1.
Технология Sound может быть реализована в рамках любого языка программирования, поэтому язык Sound можно транслировать в любой ЯП. Согласно принципу хранимой программы, всякая программа – это данные, которые могут быть обработаны транслятором. Поэтому в примере с цифрами числа массив первоначально не объявлен, и детали, относящиеся к выделению памяти, могут быть описаны вне вычислительного модуля.
Комментарии (25)
includedlibrary
16.10.2023 11:37+6Честно говоря, ничего из написанного не понял. Чем Sound отличается от любого существующего средства проверки теорем типа Coq или Agda, на которых можно формально доказывать корректность кода?
Технология Sound может быть реализована в рамках любого языка
программирования, поэтому язык Sound можно транслировать в любой ЯПЧто вообще значит это предложение? Sound - это язык или технология? Если язык, то возможность реализации компилятора Sound на языке X не доказывает возможность трасляции Sound в язык X. Если технология, то вообще не понятно, что такое Sound и как его траслировать.
В единственном приведённом примере кода не понятно, где собственно формальная верификация.
lapkin25 Автор
16.10.2023 11:37Спасибо за ответ, про саму верификацию ничего не говорилось. В рамках традиционного программирования спецификация в программу должна вводиться косвенно.
includedlibrary
16.10.2023 11:37+2Понятнее не стало. Вот, например, есть программа на си, вычисляющая сумму массива. Как мне в неё спецификацию на Sound ввести?
int sum_arr(int *arr, size_t size) { int result = 0; for(size_t i = 0; i < size; i++) result += arr[i]; return result; }lapkin25 Автор
16.10.2023 11:37func sum (a: Sequence[Range]) -> Int = { k = Range.begin s = calc_sum(a, k) = { if k == Range.end: return 0 else: return a[k] + calc_sum(a, k + 1) } return s }И дальше может потребоваться указать детали структуры данных ("внутренний интерфейс"), обозначенной через абстрактный тип Sequence, чтобы указать транслятору представление данных.
includedlibrary
16.10.2023 11:37+2Код на Sound, который вы написали, потом транслируется в код на си? Если да, то как вызывать получившуюся функцию из другого кода на си так, чтобы формальная спецификация имела смысл? Вот мы получили calc_sum, которая соответствует формальной спецификация, а потом где-то ошиблись в вызове:
int arr[12] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11}; // Тут произойдёт выход за границу массива int result = calc_sum(arr, 15);Если нет, что с ним после написания делать?
lapkin25 Автор
16.10.2023 11:37В данном случае calc_sum - это функциональный блок внутри функции sum. Это означает, что его использование предполагается только внутри функции sum, и код составлен с проверкой выхода за границы диапазона индексов. Если функция sum составлена неточно и учтены не все случаи, то это приведет к ошибке при трансляции в язык C.
includedlibrary
16.10.2023 11:37Я перепутал название функции. Я имел в виду вызов sum в коде на си.
int arr[12] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11}; // Тут произойдёт выход за границу массива int result = sum(arr, 15);lapkin25 Автор
16.10.2023 11:37В этом примере sum принимает на вход всю последовательность. Если допустить, что sum принимает на вход диапазон, то на C входные параметры превратятся в пару индексов, но в рамках Sound это будет поддиапазон, который по определению будет корректен.
includedlibrary
16.10.2023 11:37+1А можете привести пример вызова функции sum, полученной из вашего кода на си, а то я не очень понял?
lapkin25 Автор
16.10.2023 11:37int __calc_sum(int a[], int n, int k) { if (k >= n) return 0; else return a[k] + __calc_sum(a, n, k + 1); } int sum(int a[], int n) { int k = 0; int s = __calc_sum(a, n, k); return s; }
Zenitchik
16.10.2023 11:37+2В чём генеральная мысль статьи? В системе именования переменных и типов данных?
lapkin25 Автор
16.10.2023 11:37В постановке проблемы. При программировании зачастую может потеряться смысл, который вкладывается в код, если он оформлен недостаточно блочно. В дальнейшем хотелось бы добавить в язык элементы, которые помогут этого избежать.
AlexTOPMAN
16.10.2023 11:37Лично я против названия "звук" для языка, который к звуку даже отношения не имеет, но "протому что просто красиво".
cher-nov
16.10.2023 11:37+2Лично я против названия "звук" для языка, который к звуку даже отношения не имеет, но "протому что просто красиво".
Так речь здесь не про тот sound, который audio, а тот, который soundness и в "safe and sound".
Статья интересная, спасибо. Несколько пространная и путаная, но такое бывает. Поглядим, что из этого выйдет. Если я прочитал её правильно, то получается, что и сам думал над похожими вещами.
Название только и впрямь неудачное - по такому искать в интернете неудобно. Затем бренды и нужны.
habrolog
16.10.2023 11:37Так речь здесь не про тот sound, который audio, а тот, который soundness и в "safe and sound".
Отлично. И как это понять априори? Вот есть такой язык csound, 40 лет ему скоро будет, и он непосредственно про звук. И тут появляется некий sound, который не только не имеет отношения к csound, но и к звуку вообще.
funny_falcon
16.10.2023 11:37+1Почему в NumberToDigits next_digit и lowest_digit оформлены образом, похожим на функции? При этом вызова их нет. Очень запутывает. Тем более, что next_digit возвращает ok : Bool, но его использования не видно.
Кажется, что это - основная особенность языка, но в статье она не разжёвана.
lapkin25 Автор
16.10.2023 11:37Это именованные блоки, к которым не обязательно обращаться. Имя блока вводится для уточнения, что он делает, и чтобы обособить переменные, которые он использует. Переменная ok используется после блока next_digit, она указывает, следует ли завершить цикл.
funny_falcon
16.10.2023 11:37+1Если бы было ok = next_digit, я бы понял. А так вообще не понятна связь if ok и именем результирующего параметра. Почему-то с lowest_digit использовано присваивание.
lapkin25 Автор
16.10.2023 11:37Насколько допустимо такое сокращение - это сделано, чтобы не дублировать имена переменных внутри блока и вне него.
Zenitchik
Где почитать спеку языка?
lapkin25 Автор
В разработке. Пока спецификация - только в примерах.
Zenitchik
Толку от примера, который я даже прочитать не могу, потому что синтаксис не понимаю?
lapkin25 Автор
Синтаксис пока можно считать плавающим.