Войти
| Парадигма | мультипарадигма : функциональная, императивная |
|---|---|
| Разработана | в Бостонском университете |
| Стабильная версия | ATS2- 0.3.13 / 16 февраля 2019 г.; 19 месяцев назад (16.02.2019) |
| Печатная дисциплина | статическая |
| Лицензия | GPLv3 |
| Расширения имен файлов | .sats,.dats,.cats, hats. |
| Веб-сайт | http://www.ats-lang.org/ |
| Под влиянием | |
| Dependent ML, ML, OCaml, C ++ | |
ATS(Прикладной тип System) - это язык программирования, предназначенный для объединения программирования с формальной спецификацией. В ATS есть поддержка для объединения доказательства теорем с практическим программированием за счет использования передовых систем типов . Предыдущая версия The Computer Language Benchmarks Game продемонстрировала, что производительность ATS сопоставима с производительностью языков программирования C и C ++. Используя доказательство теорем и строгую проверку типов, компилятор может обнаружить и доказать, что реализованные в нем функции не подвержены ошибкам, таким как деление на ноль, утечка памяти, переполнение буфера и другие формы повреждения памяти путем проверки арифметики указателя и подсчета ссылок перед компиляцией программы. Кроме того, используя интегрированную систему доказательства теорем ATS (ATS / LF), программист может использовать статические конструкции, которые переплетаются с рабочим кодом, чтобы доказать, что функция соответствует своей спецификации.
ATS в основном является производным от языков программирования ML и OCaml. Более ранний язык Dependent ML того же автора был включен в этот язык.
Последняя версия ATS1 (Anairiats) была выпущена как v0.2.12 20 января 2015 года. Первая версия ATS2 (Postiats) была выпущена в сентябре 2013 года.
Основное внимание ATS уделяет поддержке доказательства теорем в сочетании с практическим программированием. С помощью доказательства теорем можно доказать, например, что реализованная функция не вызывает утечек памяти. Это также предотвращает другие ошибки, которые иначе могли бы быть обнаружены только во время тестирования. Он включает в себя систему, аналогичную системам помощников по доказательству, которые обычно направлены только на проверку математических доказательств, за исключением того, что ATS использует эту способность, чтобы доказать, что реализации его функций работают правильно и дают ожидаемый результат.
В качестве простого примера, в функции, использующей деление, программист может доказать, что делитель никогда не будет равен нулю, предотвращая ошибку деления на ноль. Скажем, делитель «X» был вычислен как 5-кратная длина списка «A». Можно доказать, что в случае непустого списка «X» не равно нулю, так как «X» является произведением двух ненулевых чисел (5 и длины «A»). Более практическим примером может быть доказательство с помощью подсчета ссылок, что счетчик сохранения в выделенном блоке памяти подсчитывается правильно для каждого указателя. Тогда можно будет знать и буквально доказать, что объект не будет освобожден преждевременно и что утечек памяти не произойдет.
Преимущество системы ATS состоит в том, что поскольку все доказательства теорем происходят строго внутри компилятора, это не влияет на скорость исполняемой программы. Код ATS часто труднее скомпилировать, чем стандартный код C, но после его компиляции программист может быть уверен, что он работает правильно до степени, указанной в их доказательствах (при условии, что компилятор и система времени выполнения верны).
В ATS доказательства отделены от реализации, поэтому можно реализовать функцию, не доказывая ее, если программист того пожелает.
По словам автора (Хунвэй Си), эффективность ATS во многом обусловлена способом представления данных на языке и оптимизацией хвостового вызова ( которые обычно важны для эффективности языков функционального программирования). Данные могут храниться в плоском или распакованном представлении, а не в коробочном представлении.
datapropвыражает предикаты как алгебраические типы.
Предикаты в псевдокоде, во многом похожие в источник ATS (действительный источник ATS см. ниже):
FACT (n, r) iff fact (n) = r MUL (n, m, prod) iff n * m = prod FACT (n, r) = FACT (0, 1) | FACT (n, r), если и только если FACT (n-1, r1) и MUL (n, r1, r) // для n>0 // выражает fact (n) = r iff 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). Доказательства выражают предикаты предложения.
[ФАКТ (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
На заметку:
{...} универсальная квантификация [...] экзистенциальная квантификация (... |...) (доказательство | значение) @ (...) плоский кортеж или кортеж параметров функции с переменным числом аргументов. <...>. метрика завершения#include "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: 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)) реализация main0 (argc, argv ) = {val () = if (argc! = 2) то prerrln! ("Использование:", argv [0], "") val () = assert (argc>= 2) val n0 = g0string2int (argv [1]) val n0 = g1ofg0 (n0) val () = assert (n0>= 0) val (_ (* pf *) | res) = fact (n0) val ((* void *)) = println! ("fact (", n0, ") =", res)} Все это можно добавить в один файл и скомпилировать следующим образом. Компиляция должна работать с различными внутренними компиляторами C, например gcc. Сборка мусора не используется, если явно не указано в -D_ATS_GCATS)
$ patscc fact1.dats -o fact1 $./fact1 4
компилируется и дает ожидаемый результат
val x: @ (int, char) = @ ( 15, 'c') // x.0 = 15; x.1 = 'c' val @ (a, b) = x // привязка сопоставления с образцом, a = 15, b = 'c' val x = @ { first = 15, second = 'c'} // x.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; x.1 = 'c' val '(a, b) = x // a = 15, b =' c 'val x =' {first = 15, second = 'c'} // x.first = 15 val '{first = a, second = b} = x // a = 15, b =' c 'val' {second = b,...} = x // b = 'c'С '|' вместо s eparator, некоторые функции возвращают значение результата с оценкой предикатов
val(predicate_proofs | values) = myfunct params
{...} универсальная количественная оценка [...] экзистенциальная количественная оценка (...) выражение в скобках или кортеж (... |...) (доказательства | значения).<...>. метрика завершения @ (...) плоский кортеж или вариативная функция параметры кортежа (см. пример printf) @ [byte] [BUFLEN] тип массива значений BUFLEN типа byte @ [byte] [BUFLEN] () экземпляр массива @ [byte] [BUFLEN] (0) массив инициализирован значением 0
sortdef nat = {a: int | a>= 0} // из прелюдии: ∀ '' a '' ∈ int... typedef String = [a: nat] string (a) // [..]: ∃ '' a '' ∈ nat...// {..}: ∀ a, b ∈ type... fun {a, b: type} swap_type_type (xy: @ (a, b)): @ (b, a) = (xy.1, xy.0)fun {a: t @ ype} ptr_get0 {l: addr} (pf: a @ l | p: ptr l): @ (a @ l | a) fun {a: t @ ype} ptr_set0 {l: addr} (pf: a? @ l | p: ptr l, x: a): @ (a @ l | void)viewdef array_v (a: viewt @ ype, n: int, l: addr) = @ [a] [n] @ l
как в case +, val +, type +, viewtype +,...
staload " foo.sats "// foo.sats загружается, а затем открывается в текущем пространстве имен staload F =" foo.sats "// для использования идентификаторов, квалифицированных как $ F.bar dynload" foo.dats "// загружается динамически при запуске- time
Представления данных часто объявляются для кодирования рекурсивно определенных отношений на линейных ресурсах.
представления данных 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))
Datatypes
datatype workday = Mon | Вт | Ср | Чт | Пт
списки
типы данных list0 (a: t @ ype) = list0_cons (a) of (a, list0 a) | list0_nil (a)
Тип просмотра данных похож на тип данных, но является линейным. С типом просмотра данных программист может явно освободить (или освободить) безопасным образом память, используемую для хранения конструкторов, связанных с типом просмотра данных.
локальные переменные
var res: int with pf_res = 1 // вводит pf_res как псевдоним представления @ (res)
при выделении массива стека:
#define BUFLEN 10 var! p_buf with pf_buf = @ [byte] [BUFLEN] (0) // pf_buf = @ [byte] [BUFLEN] (0) @ p_buf
См. объявления val и var
 | В Wikibooks есть книга по теме: ATS: Программирование с доказательством теорем |
