ATS (язык программирования) - ATS (programming language)

АТС
Логотип ATS.svg
Парадигмамультипарадигма: функциональный, императив
РазработаноХунвэй Си в Бостонский университет
Стабильный выпуск
ATS2-0.4.2[1] / 14 ноября 2020 г.; 24 дней назад (2020-11-14)
Печатная дисциплинастатический
ЛицензияGPLv3
Расширения имени файла.sats, .dats, шляпы.
Интернет сайтhttp://www.ats-lang.org/
Под влиянием
Зависимый ML, ML, OCaml, C ++

АТС (Система прикладных типов) - это язык программирования, предназначенный для объединения программирования с формальной спецификацией. В ATS есть поддержка объединения доказательства теорем с практическим программированием за счет использования расширенных системы типов.[2] Прошлая версия Игра "Тесты компьютерного языка" продемонстрировал, что производительность ATS сопоставима с характеристиками C и C ++ языки программирования.[3] Используя доказательство теорем и строгую проверку типов, компилятор может обнаружить и доказать, что его реализованные функции не подвержены таким ошибкам, как деление на ноль, утечки памяти, переполнение буфера, и другие формы повреждение памяти путем проверки арифметика указателя и подсчет ссылок перед компиляцией программы. Кроме того, используя интегрированную систему доказательства теорем ATS (ATS / LF), программист может использовать статические конструкции, которые переплетаются с рабочим кодом, чтобы доказать, что функция соответствует своей спецификации.

История

САР происходит в основном из ML и OCaml языки программирования. Более ранний язык, Зависимый ML, тем же автором была включена в язык.

Последняя версия ATS1 (Anairiats) была выпущена как v0.2.12 20 января 2015 года.[4] Первая версия ATS2 (Postiats) была выпущена в сентябре 2013 года.[5]

Доказательство теорем

Основная задача ATS - поддержка доказательство теорем в сочетании с практическим программированием.[2] С помощью доказательства теорем можно доказать, например, что реализованная функция не вызывает утечек памяти. Это также предотвращает другие ошибки, которые иначе могли бы быть обнаружены только во время тестирования. Он включает в себя систему, аналогичную системе помощники доказательства которые обычно направлены только на проверку математических доказательств, за исключением того, что ATS использует эту способность, чтобы доказать, что реализации его функций работают правильно и дают ожидаемый результат.

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

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

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

Представление данных

По мнению автора (Хунвэй Си), эффективность АТС[6] во многом связано с тем, как данные представлены на языке и оптимизация хвостового вызова (которые обычно важны для эффективности языков функционального программирования). Данные могут храниться в плоском или распакованном представлении, а не в коробочном представлении.

Доказательство теорем: вводный случай

Предложения

датапроп выражает предикаты в качестве алгебраические типы.

Предикаты в псевдокоде несколько похожи на источник ATS (действительный источник ATS см. Ниже):

 ФАКТ (n, r) если только    fact (n) = r MUL (n, m, prod) если только    n * m = prod FACT (n, r) = FACT (0, 1) | FACT (n, r) тогда и только тогда, когда FACT (n-1, r1) и MUL (n, r1, r) // для n> 0 // выражает факт (n) = r если только  r = n * r1 и r1 = fact (n-1)

В коде ATS:

 датапроп ФАКТ (int, int) =   | FACTbas (0, 1)             // базовый дело: ФАКТ(0, 1)   | {п:int | п > 0} {р,r1:int} // индуктивный дело     FACTind (п, р) из (ФАКТ (п-1, r1), MUL (п, r1, р))

где FACT (int, int) - тип доказательства

Пример

Не хвостовой рекурсивный факториал с предложением или "Теорема "доказывая строительство датапроп.

Оценка fact1 (n-1) возвращает пару (proof_n_minus_1 | result_of_n_minus_1), которая используется при вычислении fact1 (n). Доказательства выражают предикаты предложения.

Часть 1 (алгоритм и предложения)

 [FACT (n, r)] подразумевает [fact (n) = r] [MUL (n, m, prod)] подразумевает [n * m = prod]
 FACT (0, 1) FACT (n, r) тогда и только тогда, когда FACT (n-1, r1) и MUL (n, r1, r) для всех n> 0

Помнить:

{...} универсальная количественная оценка [...] экзистенциальная количественная оценка (... | ...) (доказательство | значение) @ (...) плоский кортеж или набор параметров функции с переменным числом аргументов. <...>. показатель завершения[7]
#включают "share / atspre_staload.hats"датапроп ФАКТ (int, int) =  | FACTbas (0, 1) из () // базовый дело  | {п:нац}{р:int}       // индуктивный дело    FACTind (п+1, (п+1)*р) из (ФАКТ (п, р))(* обратите внимание, что int (x), также int x, является моноценным типом значения int x. Сигнатура функции ниже говорит: forall n: nat существует r: int, где fact (num: int (n)) возвращает (FACT (n, r) | int (r)) *)весело факт{п:нац} .<п>. (п: int (п)) : [р:int] (ФАКТ (п, р) | int(р)) =(  если случай  | п > 0 => ((FACTind(pf1) | п * r1)) куда   {     вал (pf1 | r1) = факт (п-1)  }  | _(*еще*) => (FACTbas() | 1))

Часть 2 (процедуры и тест)

воплощать в жизнь main0 (argc, argv) ={  вал () = если (argc != 2) тогда prerrln! ("Использование: ", argv[0], "<целое число>")  вал () = утверждать (argc >= 2)  вал n0 = g0string2int (argv[1])  вал n0 = g1ofg0 (n0)  вал () = утверждать (n0 >= 0)  вал (_(*ПФ*) | res) = факт (n0)  вал ((*пустота*)) = println! ("факт(", n0, ") = ", res)}

Все это можно добавить в один файл и скомпилировать следующим образом. Компиляция должна работать с различными внутренними компиляторами C, например gcc. Вывоз мусора не используется, если явно не указано с -D_ATS_GCATS)[8]

$ patscc fact1.dats -o fact1$ ./fact1 4

компилирует и дает ожидаемый результат

Функции

Основные типы

  • bool (истина, ложь)
  • int (литералы: 255, 0377, 0xFF), унарный минус как ~ (как в ML )
  • двойной
  • char 'a'
  • строка "abc"

Кортежи и записи

префикс @ или none означает прямой, плоский или распакованное распределение
  вал Икс : @(int, char) = @(15, 'c')  // Икс.0 = 15 ; Икс.1 = 'c'  вал @(а, б) = Икс                    // шаблон соответствие привязка, а= 15, б='c'  вал Икс = @{первый=15, второй='c'}    // Икс.первый = 15  вал @{первый=а, второй=б} = Икс       // а= 15, б='c'  вал @{второй=б, ...} = Икс           // с упущение, б='c'
префикс 'означает косвенное или выделенное в рамку распределение
  вал Икс : '(int, char) = '(15, 'c')  // Икс.0 = 15 ; Икс.1 = 'c'  вал '(а, б) = Икс                    // а= 15, б='c'  вал Икс = '{первый=15, второй='c'}    // Икс.первый = 15  вал '{первый=а, второй=б} = Икс       // а= 15, б='c'  вал '{второй=б, ...} = Икс           // б='c'
специальный

С помощью '|' в качестве разделителя некоторые функции возвращают значение результата с оценкой предикатов

вал (predicate_proofs | значения) = параметры myfunct

Общий

{...} универсальная количественная оценка [...] экзистенциальная количественная оценка (...) выражение в скобках или кортеж (... | ...) (доказательства | значения)
. <...>. метрика завершения @ (...) плоский кортеж или вариативная функция набор параметров (см. примеры printf) @ [byte] [BUFLEN] тип массива значений BUFLEN типа байт[9]@ [byte] [BUFLEN] () экземпляр массива @ [byte] [BUFLEN] (0) массив, инициализированный 0

Словарь

Сортировать
домен
 sortdef нац = {а: int | а >= 0 }     // из прелюдия: ∀ ''а'' ∈ int ... typedef Нить = [а:нац] нить(а)   // [..]: ∃ ''а'' ∈ нац ...
тип (как сортировка)
общий Сортировать для элементов с длиной слова-указателя, которые будут использоваться в параметризованных полиморфных функциях. Также "коробочные типы"[10]
// {..}: ∀ a, b ∈ type ... fun {a, b: type} swap_type_type (xy: @ (a, b)): @ (b, a) = (xy.1, xy. 0)
тип
линейная версия предыдущего тип с абстрактной длиной. Также распакованные типы.[10]
вид
класс домена, например тип с Посмотреть (ассоциация памяти)
просмотр @ ype
линейная версия вид с абстрактной длиной. Это суперсеты вид
Посмотреть
отношение Типа и места в памяти. Инфикс @ - его самый распространенный конструктор
T @ L утверждает, что есть вид типа T в местоположении L
 весело {а:т@ype} ptr_get0 {л:адрес} (ПФ: а @ л | п: ptr л): @(а @ л | а)  весело {а:т@ype} ptr_set0 {л:адрес} (ПФ: а? @ л | п: ptr л, Икс: а): @(а @ л | пустота)
тип ptr_get0 (T) - ∀ l: addr. (T @ l | ptr (l)) -> (T @ l | T) // см. Руководство, раздел 7.1. Безопасный доступ к памяти через указатели[11]
viewdef array_v (a: viewt @ ype, n: int, l: addr) = @ [a] [n] @ l
Т?
возможно неинициализированный тип

исчерпывающее количество сопоставлений с образцом

как в чехол +, val +, тип +, viewtype +, ...

  • с суффиксом '+' компилятор выдает ошибку в случае неполных альтернатив
  • без суффикса компилятор выдает предупреждение
  • с суффиксом '-', избегает контроля исчерпываемости

модули

 staload "foo.sats" // foo.sats загружается и затем открывается в текущем пространстве имен staload F = "foo.sats" // для использования идентификаторов, квалифицированных как $ F.bar dynload "foo.dats" // загружается динамически в время выполнения

просмотр данных

Представления данных часто объявляются для кодирования рекурсивно определенных отношений на линейных ресурсах.[12]

dataview array_v (a: viewt @ ype +, int, addr) = | {l: addr} array_v_none (a, 0, l) | {n: nat} {l: addr} array_v_some (a, n + 1, l) of (a @ l, array_v (a, n, l + sizeof a))

тип данных / тип просмотра данных

Типы данных[13]

тип данных рабочий день = Пн | Вт | Ср | Чт | Пт

списки

тип данных list0 (a: t @ ype) = list0_cons (a) of (a, list0 a) | list0_nil (а)

dataviewtype

Тип просмотра данных похож на тип данных, но является линейным. С помощью dataviewtype программист может явно освободить (или освободить) безопасным способом память, используемую для хранения конструкторов, связанных с dataviewtype.[14]

переменные

локальные переменные

var res: int with pf_res = 1 // вводит pf_res как псевдоним просмотр @ (разрешение)

в стеке размещение массива:

#define BUFLEN 10var! p_buf with pf_buf = @ [byte] [BUFLEN] (0) // pf_buf = @ [byte] [BUFLEN] (0) @ p_buf[15]

Видеть вал и вар декларации[16]

Рекомендации

  1. ^ Hongwei Xi (14 ноя 2020). "[ats-lang-users] Выпущен ATS2-0.4.2". ats-lang-users. Получено 17 ноя 2020.
  2. ^ а б Объединение программирования с доказательством теорем
  3. ^ Тесты ATS | Компьютерная языковая тестовая игра (веб-архив)
  4. ^ https://sourceforge.net/projects/ats-lang/files/ats-lang/
  5. ^ https://github.com/githwxi/ATS-Postiats/commit/30fd556e649745f735eafbdace54373fa163862e
  6. ^ Обсуждение эффективности языка (Language Shootout: ATS - новый лучший стрелок. Превосходит C ++.)
  7. ^ Показатели завершения
  8. ^ Компиляция - Сборка мусора В архиве 4 августа 2009 г. Wayback Machine
  9. ^ тип массива В архиве 4 сентября 2011 г. Wayback Machine типа @ [T] [I]
  10. ^ а б «Введение в зависимые типы». Архивировано из оригинал на 2016-03-12. Получено 2016-02-13.
  11. ^ Руководство, раздел 7.1. Безопасный доступ к памяти через указатели[постоянная мертвая ссылка ] (устарело)
  12. ^ Конструкция Dataview В архиве 13 апреля 2010 г. Wayback Machine
  13. ^ Конструкция типа данных В архиве 14 апреля 2010 г. Wayback Machine
  14. ^ Dataviewtype конструкция
  15. ^ Руководство - 7.3 Выделение памяти в стеке В архиве 9 августа 2014 г. Wayback Machine (устарело)
  16. ^ Объявления Val и Var В архиве 9 августа 2014 г. Wayback Machine (устарело)

внешняя ссылка