ATS (язык программирования)
Последнее изменение этой страницы: 00:50, 9 июня 2016.
Парадигма | Мультипарадигменный: императивный, функциональный |
---|---|
Спроектировано | Хунвэй Си из Бостонского университета |
Портал: | 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 может помочь научить типа теории, демонстрируя как убедительно и конкретно силу и потенциал типов в создании качественного программного обеспечения.
Особенности
Базовые типы данных
- bool (true, false) - логический тип
- int (literals: 255, 0377, 0xFF), унарный минус ~ (как в ML)
- double - вещественные числа
- char 'a' - символьный тип
- 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
ISSN 2542-0356
Следуй за Полисом
Оставайся в курсе последних событий
Лицензия
Если не указано иное, содержание этой страницы доступно по лицензии Creative Commons «Attribution-NonCommercial-NoDerivatives» 4.0, а примеры кода – по лицензии Apache 2.0. Подробнее см. Условия использования.