Пока (язык программирования)
| Парадигма | Императивный , Функциональный |
|---|---|
| Разработано | Дэвид Дж. Пирс |
| Впервые появился | июнь 2010 г. |
| Стабильная версия | 0.6.1
/ 27 июня 2022 г |
| Дисциплина набора текста | Прочный , безопасный , структурный , чувствительный к потоку |
| Лицензия | БСД |
| Веб-сайт | пока |
| Под влиянием | |
| Java , Си , Питон , Ржавчина | |
Whiley — экспериментальный язык программирования, сочетающий в себе функции функциональной и императивной парадигм и поддерживающий формальную спецификацию посредством предварительных условий функций , постусловий и инвариантов цикла . [1] В языке используется чувствительная к потоку типизация, также известная как «потоковая типизация».
Проект Whiley начался в 2009 году в ответ на «Большой вызов верификации компилятора», выдвинутый Тони Хоаром в 2003 году. [2] Первый публичный релиз Whiley состоялся в июне 2010 года. [3]
Первоначально разработанный Дэвидом Пирсом, Whiley представляет собой проект с открытым исходным кодом, созданный при участии небольшого сообщества. Система использовалась для студенческих исследовательских проектов и при преподавании студентов. [4] В период с 2012 по 2014 год его поддерживал Фонд Марсдена Королевского общества Новой Зеландии. [5]
Компилятор Whiley генерирует код для виртуальной машины Java и может взаимодействовать с Java и другими языками на основе JVM.
Обзор
[ редактировать ]Цель Whiley — предоставить реалистичный язык программирования, в котором проверка будет использоваться регулярно и без размышлений. Идея такого инструмента имеет долгую историю, но она активно продвигалась в начале 2000-х годов в рамках проекта Хоара Verifying Compiler Grand Challenge. Целью этой задачи было стимулировать новые усилия по разработке проверяющего компилятора , который примерно описывается следующим образом: [6]
Проверяющий компилятор использует математические и логические рассуждения для проверки правильности компилируемых им программ.
— Тони Хоар
Основная цель такого инструмента — улучшить качество программного обеспечения , гарантируя, что программа соответствует формальной спецификации . В то время как многие попытки разработать такие инструменты, включая такие известные усилия, как SPARK/Ada , ESC/Java , Spec#, Dafny ,Why3, [7] и Фрама-С .
Большинство предыдущих попыток разработать проверяющий компилятор были направлены на расширение существующих языков программирования конструкциями для написания спецификаций. Например, ESC/Java и язык моделирования Java добавляют в Java аннотации для указания предварительных и постусловий . Аналогично, Spec# и Frama-C добавляют аналогичные конструкции в C# и C. языки программирования Однако известно, что эти языки содержат множество особенностей, которые создают трудные или непреодолимые проблемы для проверки. [8] Напротив, язык Whiley был разработан с нуля, чтобы избежать распространенных ошибок и сделать проверку более простой. [9]
Функции
[ редактировать ]Синтаксис Whiley соответствует общему виду императивных или объектно-ориентированных языков. Синтаксис отступов выбран вместо использования фигурных скобок для разграничения блоков операторов, учитывая сильное сходство с Python . Однако императивный вид Whiley несколько вводит в заблуждение, поскольку ядро языка функционально и чисто .
Уити выделяет function (который является чистым ) из method (которые могут иметь побочные эффекты ). Это различие необходимо, поскольку оно позволяет использовать функции в спецификациях. Доступен знакомый набор примитивных типов данных, включая bool, int, массивы (например int[]) и записи (например, {int x, int y}). Однако, в отличие от большинства языков программирования, целочисленный тип данных, int, не ограничен и не соответствует представлению фиксированной ширины, такому как 32-битное дополнение до двух . Таким образом, неограниченное целое число в Whiley может принимать любое возможное целочисленное значение в зависимости от ограничений памяти хост-среды. Этот выбор упрощает проверку, поскольку рассуждения об арифметике по модулю — известная и трудная проблема. Составные объекты (например, массивы или записи) не являются ссылками на значения в куче, как в таких языках, как Java или C#, а представляют собой неизменяемые значения.
Уилли использует необычный подход к проверке типов, называемый «потоковая типизация». Переменные могут иметь разные статические типы в разных точках функции или метода. Поточная типизация аналогична типизации вхождений , используемой в Racket . [10] Чтобы облегчить типизацию потока, Whiley поддерживает типы объединения , пересечения и отрицания. [11] Типы объединения сравнимы с типами сумм, встречающимися в функциональных языках, таких как Haskell , но в Whiley они не являются непересекающимися. Типы пересечения и отрицания используются в контексте потоковой типизации для определения типа переменной в истинной и ложной ветвях проверки типа во время выполнения. Например, предположим, что переменная x типа T и тест типа времени выполнения x is S. На истинной ветви тип x становится T & S в то время как на ложной ветви он становится T & !S.
В то время как используется структурная, а не номинальная система типов. Modula-3 , Go и Ceylon — примеры других языков, которые в той или иной форме поддерживают структурную типизацию.
Whiley поддерживает время жизни ссылок, аналогичное тем, которые есть в Rust . Время жизни может быть указано при выделении новых объектов, чтобы указать, когда их можно безопасно освободить. Ссылки на такие объекты должны включать идентификатор времени жизни, чтобы предотвратить висячие ссылки . Каждый метод имеет неявное время жизни, на которое указывает this. Переменная типа &this:T представляет собой ссылку на объект типа T который освобождается с помощью заключающего метода. Подтипирование между сроками жизни определяется отношением пережитков . Таким образом, &l1:T является подтипом &l2:T если всю жизнь l1 статически переживёт время жизни l2. Говорят, что жизнь, охватывающая другую, переживет ее. Время жизни в Whiley отличается от Rust тем, что в настоящее время оно не включает в себя концепцию владения .
У Whiley нет встроенной поддержки параллелизма и формальной модели памяти, позволяющей определить, как следует интерпретировать чтение/запись в общее изменяемое состояние.
Пример
[ редактировать ]Следующий пример иллюстрирует многие интересные возможности Whiley, включая использование постусловий, инвариантов циклов, инвариантов типов, типов объединения и потоковой типизации. Функция предназначена для возврата первого индекса целого числа. item в массиве целых чисел items. Если такого индекса не существует, то null возвращается.
// Define the type of natural numbers
type nat is (int x) where x >= 0
public function indexOf(int[] items, int item) -> (int|null index)
// If int returned, element at this position matches item
ensures index is int ==> items[index] == item
// If int returned, element at this position is first match
ensures index is int ==> no { i in 0 .. index | items[i] == item }
// If null returned, no element in items matches item
ensures index is null ==> no { i in 0 .. |items| | items[i] == item }:
//
nat i = 0
//
while i < |items|
// No element seen so far matches item
where no { j in 0 .. i | items[j] == item }:
//
if items[i] == item:
return i
i = i + 1
//
return null
В приведенном выше примере объявленному типу возвращаемого значения функции присваивается тип объединения. int|null что указывает на то, либо что int значение возвращается или null возвращается. функции Постусловие состоит из трех ensures предложения, каждое из которых описывает различные свойства, которые должны содержать возвращаемые значения. index. В этих разделах типизация потока используется посредством оператора проверки типа во время выполнения: is. Например, в первом ensures предложение, переменная index перепечатано из int|null просто int в правой части оператора импликации (т.е. ==>).
Приведенный выше пример также иллюстрирует использование инварианта индуктивной петли . Должно быть показано, что инвариант цикла сохраняется при входе в цикл, для любой заданной итерации цикла и при выходе из цикла. В этом случае инвариант цикла сообщает, что известно об элементах items рассмотрено до сих пор, а именно, что ни один из них не соответствует заданному item. Инвариант цикла не влияет на смысл программы и в некотором смысле может считаться ненужным. Однако инвариант цикла необходим, чтобы помочь автоматизированному верификатору, используемому в компиляторе Whiley, доказать, что эта функция соответствует ее спецификации.
В приведенном выше примере также определяется тип nat с соответствующим инвариантом типа . Этот тип используется для объявления переменной i и указать, что он никогда не может иметь отрицательное значение. В этом случае объявление предотвращает необходимость в дополнительном инварианте цикла вида where i >= 0 что в противном случае было бы необходимо.
История
[ редактировать ]Компания Whiley начала свою деятельность в 2009 году с первого публичного релиза. v0.2.27 после в июне 2010 года и v0.3.0 в сентябре того же года. Язык развивался медленно, и на сегодняшний день в него были внесены многочисленные синтаксические изменения. Предыдущие версии v0.3.33 поддерживается первоклассный string и char типы данных, но они были удалены в пользу представления строк как ограниченных int[] массивы. Аналогично, версии до v0.3.35 поддерживается первоклассный набор (например, {int}), словарь (например {int=>bool}) и список изменяемого размера [int]), но от них отказались в пользу простых массивов (например, int[]). Пожалуй, самым спорным было удаление real тип данных в версии v0.3.38. Многие из этих изменений были мотивированы желанием упростить язык и сделать разработку компилятора более управляемой.
Еще одной важной вехой в эволюции Whiley стала версия v0.3.40 с включением эталонных времен жизни, разработанных Себастьяном Швейцером в рамках его магистерской диссертации в Университете Кайзерслаутерна .
Ссылки
[ редактировать ]- ^ «Домашняя страница Уайли» .
- ^ Хоар, Тони (2003). «Проверочный компилятор: грандиозная задача для компьютерных исследований». Журнал АКМ . 50 : 63–69. дои : 10.1145/602382.602403 . S2CID 441648 .
- ^ «Выпущена версияWhiley v0.2.27!» . Архивировано из оригинала 12 апреля 2016 г. Проверено 1 февраля 2016 г.
- ^ «пока.орг/люди» . [ постоянная мертвая ссылка ]
- ^ «Фонд Марсдена» .
- ^ Хоар, Тони (2003). «Проверочный компилятор: грандиозная задача для компьютерных исследований». Журнал АКМ . 50 : 63–69. дои : 10.1145/602382.602403 . S2CID 441648 .
- ^ «Why3 --- Где программы встречаются с пруверами» .
- ^ Барнетт, Майк; Фендрих, Мануэль; Лейно, К. Рустан М.; Мюллер, Питер; Шульте, Вольфрам; Вентер, Герман (2011). «Спецификация и проверка: опыт Spec#». Коммуникации АКМ . 54 (6): 81. дои : 10.1145/1953122.1953145 . S2CID 29809 .
- ^ Пирс, Дэвид Дж.; Гроувс, Линдси (2015). «Проектирование проверяющего компилятора: уроки, извлеченные из разработки Whiley» . Наука компьютерного программирования . 113 : 191–220. дои : 10.1016/j.scico.2015.09.006 .
- ^ «Типирование событий» .
- ^ Пирс, Дэвид (2013). «Разумная и полная потоковая типизация с союзами, пересечениями и отрицаниями» (PDF) .