16.10.2023 10:56
lapkin25 25 5700 Источник

Средство обработки унифицированных по назначению данных (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)


  1. Zenitchik
    16.10.2023 11:37
    #26062490
    +2

    Где почитать спеку языка?


    1. lapkin25 Автор
      16.10.2023 11:37
      #26062500
      -2

      В разработке. Пока спецификация - только в примерах.


      1. Zenitchik
        16.10.2023 11:37
        #26062638
        +7

        Толку от примера, который я даже прочитать не могу, потому что синтаксис не понимаю?


        1. lapkin25 Автор
          16.10.2023 11:37
          #26063468
          -2

          Синтаксис пока можно считать плавающим.


  1. includedlibrary
    16.10.2023 11:37
    #26062556
    +6

    Честно говоря, ничего из написанного не понял. Чем Sound отличается от любого существующего средства проверки теорем типа Coq или Agda, на которых можно формально доказывать корректность кода?

    Технология Sound может быть реализована в рамках любого языка
    программирования, поэтому язык Sound можно транслировать в любой ЯП

    Что вообще значит это предложение? Sound - это язык или технология? Если язык, то возможность реализации компилятора Sound на языке X не доказывает возможность трасляции Sound в язык X. Если технология, то вообще не понятно, что такое Sound и как его траслировать.

    В единственном приведённом примере кода не понятно, где собственно формальная верификация.


    1. lapkin25 Автор
      16.10.2023 11:37
      #26063480

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


      1. includedlibrary
        16.10.2023 11:37
        #26063664
        +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;
}


        1. lapkin25 Автор
          16.10.2023 11:37
          #26063720

          func 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, чтобы указать транслятору представление данных.


          1. includedlibrary
            16.10.2023 11:37
            #26063746
            +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);

            Если нет, что с ним после написания делать?


            1. lapkin25 Автор
              16.10.2023 11:37
              #26063778

              В данном случае calc_sum - это функциональный блок внутри функции sum. Это означает, что его использование предполагается только внутри функции sum, и код составлен с проверкой выхода за границы диапазона индексов. Если функция sum составлена неточно и учтены не все случаи, то это приведет к ошибке при трансляции в язык C.


              1. includedlibrary
                16.10.2023 11:37
                #26063790

                Я перепутал название функции. Я имел в виду вызов sum в коде на си.

                int arr[12] = {0, 1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11};
// Тут произойдёт выход за границу массива
int result = sum(arr, 15);


                1. lapkin25 Автор
                  16.10.2023 11:37
                  #26063802

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


                  1. includedlibrary
                    16.10.2023 11:37
                    #26063842
                    +1

                    А можете привести пример вызова функции sum, полученной из вашего кода на си, а то я не очень понял?


                    1. lapkin25 Автор
                      16.10.2023 11:37
                      #26063882

                      int __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;
}


  1. Zenitchik
    16.10.2023 11:37
    #26063068
    +2

    В чём генеральная мысль статьи? В системе именования переменных и типов данных?


    1. lapkin25 Автор
      16.10.2023 11:37
      #26063474

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


      1. Zenitchik
        16.10.2023 11:37
        #26063524
        +4

        Тогда статья провальная. Проблема толком не сформулирована. Элементы, которые нужно добавить в язык - не названы. Много словоблудия и непонятный код.


        1. Tzimie
          16.10.2023 11:37
          #26064058
          +2

          Она невнятная)


  1. AlexTOPMAN
    16.10.2023 11:37
    #26064038

    Лично я против названия "звук" для языка, который к звуку даже отношения не имеет, но "протому что просто красиво".


    1. cher-nov
      16.10.2023 11:37
      #26064062
      +2

      Лично я против названия "звук" для языка, который к звуку даже отношения не имеет, но "протому что просто красиво".

      Так речь здесь не про тот sound, который audio, а тот, который soundness и в "safe and sound".

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

      Название только и впрямь неудачное - по такому искать в интернете неудобно. Затем бренды и нужны.


      1. habrolog
        16.10.2023 11:37
        #26065712

        Так речь здесь не про тот sound, который audio, а тот, который soundness и в "safe and sound".

        Отлично. И как это понять априори? Вот есть такой язык csound, 40 лет ему скоро будет, и он непосредственно про звук. И тут появляется некий sound, который не только не имеет отношения к csound, но и к звуку вообще.


  1. funny_falcon
    16.10.2023 11:37
    #26065206
    +1

    Почему в NumberToDigits next_digit и lowest_digit оформлены образом, похожим на функции? При этом вызова их нет. Очень запутывает. Тем более, что next_digit возвращает ok : Bool, но его использования не видно.

    Кажется, что это - основная особенность языка, но в статье она не разжёвана.


    1. lapkin25 Автор
      16.10.2023 11:37
      #26065282

      Это именованные блоки, к которым не обязательно обращаться. Имя блока вводится для уточнения, что он делает, и чтобы обособить переменные, которые он использует. Переменная ok используется после блока next_digit, она указывает, следует ли завершить цикл.


      1. funny_falcon
        16.10.2023 11:37
        #26065366
        +1

        Если бы было ok = next_digit, я бы понял. А так вообще не понятна связь if ok и именем результирующего параметра. Почему-то с lowest_digit использовано присваивание.


        1. lapkin25 Автор
          16.10.2023 11:37
          #26065442

          Насколько допустимо такое сокращение - это сделано, чтобы не дублировать имена переменных внутри блока и вне него.