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

ATS ( Applied Type System ) - это язык программирования, предназначенный для объединения программирования с формальной спецификацией. ATS поддерживает объединение доказательства теорем с практическим программированием за счет использования передовых систем типов . [2] Прошлая версия игры The Computer Language Benchmarks Game продемонстрировала, что производительность ATS сопоставима с производительностью языков программирования C и C ++ . [3] Используя доказательство теорем и строгую проверку типов, компилятор может обнаружить и доказать, что его реализованные функции не подвержены ошибкам, таким как деление на ноль , утечки памяти и т. Д.переполнение буфера и другие формы повреждения памяти путем проверки арифметики указателя и подсчета ссылок перед компиляцией программы. Кроме того, используя интегрированную систему доказательства теорем ATS (ATS / LF), программист может использовать статические конструкции, которые переплетаются с оперативным кодом, чтобы доказать, что функция соответствует своей спецификации.

История [ править ]

ATS в основном является производным от языков программирования ML и OCaml . Более ранний язык, Dependent 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 доказательства отделены от реализации, поэтому при желании программиста можно реализовать функцию, не доказывая ее.

Представление данных [ править ]

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

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

Предложения [ править ]

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

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

FACT (n, r) тогда и только тогда, когда fact (n) = r MUL (n, m, prod) тогда и только тогда, когда n * m = prod  ФАКТ (n, r) =  ФАКТ (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:

 dataprop  FACT  ( int ,  int )  =  |  FACTbas  ( 0 ,  1 )  //  базовый  случай :  FACT ( 0 ,  1 )  |  { n : int  |  n  >  0 }  { r , r1 : int }  //  индуктивный  случай  FACTind  ( n ,  r )  of  ( FACT  ( n -1 ,  r1 ),  MUL  ( n ,  r1 ,  r ))

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

Пример [ править ]

Не хвостовой рекурсивный факториал с утверждением или " теоремой ", доказываемой через конструкцию dataprop .

Оценка 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]
 ФАКТ (0, 1) FACT (n, r) тогда и только тогда, когда FACT (n-1, r1) и MUL (n, r1, r) для всех n> 0

Помнить:

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

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

реализовать  main0  ( argc ,  argv )  = {  val  ()  =  if  ( argc  ! =  2 )  then  prerrln !  ( "Использование:" ,  argv [ 0 ],  "<целое число>" ) val  ()  =  assert  ( argc  > =  2 )  val  n0  =  g0string2int  ( argv [ 1 ])  val  n0  =  g1ofg0  ( n0 )  val  ()  =  assert  ( n0  > =  0 )  val  (_ (* pf *)  |  res )  =  факт  ( n0 ) val  ( (* void *) )  =  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 означает прямое, плоское или распакованное распределение
 val  x  :  @ ( int ,  char )  =  @ ( 15 ,  'c' )  //  x . 0  =  15  ;  х . 1  =  'с'  Val  @ ( , б ) = х // шаблон согласования связывания , а = 15 , б = 'с' Val х = @ { первый = 15 , второй = 'C'               }  //  х . first  =  15  val  @ { first = a ,  second = b }  =  x  //  a =  15 ,  b = 'c'  val  @ { second = b ,  ...}  =  x  //  с  пропуском ,  b = 'c'
префикс 'означает косвенное или выделенное в рамку распределение
 val  x  :  ' ( int ,  char )  =  ' ( 15 ,  'c' )  //  x . 0  =  15  ;  х . 1  =  'c'  val  ' ( a ,  b )  =  x  //  a =  15 ,  b = ' c '  val  x  =  ' { first = 15 ,  second = 'c' } //  х . first  =  15  val  ' { first = a ,  second = b }  =  x  //  a =  15 ,  b = ' c '  val  ' { second = b ,  ...}  =  x  //  b = 'c'
специальный

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

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

Общие [ править ]

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

Словарь [ править ]

Сортировать
домен
 sortdef  nat  =  { a :  int  |  a  > =  0  }  //  из  прелюдии :  ∀  ' ' a ' '  ∈  int  ... typedef  String  =  [ a : nat ]  string ( a )  //  [..]:  ∃  ' ' a ' '  ∈  nat  ...
тип (как сортировка)
общая сортировка для элементов с длиной слова-указателя, которая будет использоваться в параметризованных полиморфных функциях. Также «коробочные типы» [10]
// {..}: ∀ a, b ∈ type ...fun {a, b: type} swap_type_type (xy: @ (a, b)): @ (b, a) = (xy.1, xy.0)
тип
линейная версия предыдущего типа с абстрактной длиной. Также распакованные типы. [10]
вид
класс предметной области, такой как тип с представлением (ассоциация памяти)
просмотр @ ype
линейная версия viewtype с абстрактной длиной. Он расширяет вид
Посмотреть
отношение Типа и места в памяти. Инфикс @ - его самый распространенный конструктор.
T @ L утверждает, что есть вид типа T в местоположении L
 весело  { : т @ ип } ptr_get0 { л : адр } ( пф : @ л | р : PTR л ): @ ( @ л | )                 весело  { : т @ ип } 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 + , type + , viewtype + , ...

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

модули [ править ]

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

dataview [ править ]

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

dataview array_v (a: viewt @ ype +, int, addr) = | {l: addr} array_v_none (a, 0, l) | {n: nat} {l: addr} массив_v_some (a, n + 1, l) из (a @ l, array_v (a, n, l + sizeof a))

datatype / dataviewtype [ править ]

Типы данных [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 как псевдоним представления @ (res)

при выделении массива стека :

#define БУФЛЕН 10var! p_buf с pf_buf = @ [byte] [BUFLEN] (0) // pf_buf = @ [byte] [BUFLEN] (0) @ p_buf [15]

См. Объявления val и var [16]

Ссылки [ править ]

  1. ^ Hongwei Xi (14 ноября 2020). "[ats-lang-users] Выпущен ATS2-0.4.2" . ats-lang-users . Проверено 17 ноя 2020 .
  2. ^ a b Объединение программирования с доказательством теорем
  3. ^ Тесты ATS | Игра Computer Language Benchmarks (веб-архив)
  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. ^ a b «Введение в зависимые типы» . Архивировано из оригинала на 2016-03-12 . Проверено 13 февраля 2016 .
  11. ^ Руководство, раздел 7.1. Безопасный доступ к памяти через указатели [ постоянная неработающая ссылка ] (устарело)
  12. ^ DataView конструкт архивации 13 апреля 2010, в Wayback Machine
  13. ^ Datatype конструкт архивации 14 апреля 2010, в Wayback Machine
  14. ^ Конструкция Dataviewtype
  15. ^ Руководство - 7.3 Распределение памяти в стеке. Архивировано 9 августа 2014 г. на Wayback Machine (устарело).
  16. ^ Val и вар деклараций архивации 9 августа 2014, в Wayback Machine (устаревший)

Внешние ссылки [ править ]

  • Домашняя страница ATS
  • Документация по языку программирования ATS для ATS2
  • Старая документация по языку программирования ATS для ATS1
  • Ручной черновик (устаревший). Некоторые примеры относятся к функциям или подпрограммам, отсутствующим в выпуске (Anairiats-0.1.6) (например: перегрузка печати для strbuf, и использование его примеров массивов дает ошибки типа «использование подписки на массив не поддерживается»).
  • ATS для программистов ML
  • Обучающие примеры и краткие примеры использования ATS