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

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

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

• ATS benchmarks | Computer Language Benchmarks Game
• Discussion about the language’s efficiency (Language Shootout: ATS is the new top gunslinger. Beats C++.)
• Combining Programming with Theorem Proving