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

Материал из Национальной библиотеки им. Н. Э. Баумана
Последнее изменение этой страницы: 00:50, 9 июня 2016.
ATS
Парадигма Мультипарадигменный: императивный, функциональный
Спроектировано Хунвэй Си из Бостонского университета
Портал: http://www.ats-lang.org/

Что такое ATS

ATS - это статически типизированный язык программирования, который объединяет реализацию с формальной спецификацией. Он оснащен весьма выразительный системой типов, которая и дает языку его имя. В частности, оба составные и простые типы доступны в ATS.

Текущая реализация ATS2 написанная на ATS1, состоящий из более чем 150К строк кода. ATS может быть столь же эффективным, как Си/Си++ используя умные указатели и подсчет ссылок и поддерживает различные парадигмы программирования, которые включают:

  • Функционального программирования. Ядром ATS является вызов по значению, функциональный язык вдохновленный ML. Наличие простых типов в САР часто делает функциональные программы, написанные на нем, не только удивительно эффективными (по сравнению с), но и расходующими удивительно мало памяти по сравнению с Си.
  • Императивное программирование. Новым подходом к императивному программированию в ATS прочно укоренился в парадигме программирования с доказательством теорем. Система типов АТS позволяет использовать многие функции, которые считаются опасными в других языках (таких как явные арифметические операции над указателями и эксплицитной памяти выделение/освобождение памяти). ATS архитектура хорошо подходит для реализации высококачественных низкоуровневых систем.
  • Параллельное программирование. ATS может поддерживать многопоточное программирование через безопасное использование pthreads. Наличие простого типа для отслеживания и манипуляции ресурсами обеспечивает эффективный подход к построению надежных программ, что может дать большое преимущество в многоядерных архитектурах.
  • Модульное программирование. Модуль системы ATS во многом схож с Модула-3, которая является одновременно простой и общей, а также эффективно поддерживать крупномасштабное программирование.

Кроме того, ATS содержит подсистему ATS/LF, которая поддерживает форму (интерактивного) доказательства теорем, где доказательства строятся как общие функции. Этой подсистемой ATS может выступать программно-ориентированный подход к верификации программ, который совмещает программирование с помощью доказательства теорем и синтаксическим образом переплелись. Кроме того, ATS/LF может служить как логическая структура для кодирования различных формальных систем (таких, как логика системы и системы типов) вместе с доказательствами их (Мета)свойствах.

История

ATS происходит в основном из ML и OCaml языков программирования. Ранее зависимости разработанные автором языка были включены в язык программирования ML.

Для чего хорош ATS?

  • ATS можно использовать для достижения точности в практическом программировании.
  • ATS можно использовать для ускорения разработки программного обеспечения.
  • ATS позволяет программисту писать эффективные функциональные программы, которые непосредственно управляют своими представлениями данных.
  • ATS позволяет программисту сократить объем памяти, занимаемой программой, путем использования простого типов.
  • ATS позволяет программисту повысить безопасность (и эффективность) программы путем использования доказательства теорем.
  • ATS позволяет программисту писать безопасный код нижнего уровня, который выполняется в ядре ОС.
  • ATS может помочь научить типа теории, демонстрируя как убедительно и конкретно силу и потенциал типов в создании качественного программного обеспечения.

Особенности

Базовые типы данных

  1. bool (true, false) - логический тип
  2. int (literals: 255, 0377, 0xFF), унарный минус ~ (как в ML)
  3. double - вещественные числа
  4. char 'a' - символьный тип
  5. string "abc" - строковый тип

Картежи и структуры

Префикс @ or его отсутствие означают выделение на стеке или в куче без освобождения:

 
 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'

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

  val ( predicate_proofs | values) = myfunct params

Общие

{...} универсальный количественный параметр
[...] экзистенциальный количественный параметр
(...) выражение в скобках или кортеж

(... | ...)     (доказательство | значение)
@[byte][BUFLEN]     массив BUFLEN значений типа byte 
@[byte][BUFLEN]()   создание массива
@[byte][BUFLEN](0)  создание массива инициализированного нулями

Словарь

sort
domain
sortdef nat = {a: int | a >= 0 }     // для значений: ∀ a ∈ int ...
typedef String = [a:nat] string(a)   // [..]: ∃ a ∈ nat ...
type (as sort)
генерация sort для элементов длиной со слово, использовать как тип полиморфной функции.
// {..}: ∀ a,b ∈ type ...
fun {a,b:type} swap_type_type (xy: @(a, b)): @(b, a) = (xy.1, xy.0)
t@ype
аналог предыдущего типа, где type имеет неизвестный размер.
viewtype
тип похожий на type с view
viewt@ype
простая версия viewtype с неизвестной длинной. Это надмножество над viewtype
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)
тип ptr_get0 (T) is ∀ l : addr . ( T @ l | ptr( l ) ) -> ( T @ l | T)
viewdef array_v (a:viewt@ype, n:int, l: addr) = @[a][n] @ l
T? 
тип может быть неинициализированным

Модули

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

Переменные

  • локальная переменная
var res: int with pf_res = 1   // pf_res используется как алиас с view @ (res)
  • массив выделенный на стеке:
#define BUFLEN 10
var !p_buf with pf_buf = @[byte][BUFLEN](0)    // pf_buf = @[byte][BUFLEN](0) @ p_buf

Список литературы