Хореографическое программирование
В информатике хореографическое программирование — это парадигма программирования , в которой программы представляют собой композиции взаимодействий между несколькими одновременно работающими участниками. [1] [2] [3]
Обзор [ править ]
Хореография [ править ]
В хореографическом программировании разработчики используют язык хореографического программирования для определения предполагаемого коммуникативного поведения одновременных участников. Программы в этой парадигме называются хореографиями . [1] Хореографические языки основаны на нотации протокола безопасности (также известной как нотация «Алисы и Боба»). Ключом к этим языкам является примитив общения, например
Alice.expr -> Bob.x
читает " Alice сообщает результат вычисления выражения expr к Bob, который сохраняет его в своей локальной переменной x". [3]
Алису, Боба и т. д. обычно называют ролями или процессами . [2]
В приведенном ниже примере показана хореография упрощенного протокола единого входа (SSO) на основе центральной службы аутентификации (CAS), которая включает в себя три роли:
Client, который хочет получить токен доступа отCASвзаимодействовать сService.Service, что необходимо знать изCASеслиClientдолжен быть предоставлен доступ.CAS, которая является центральной службой аутентификации, ответственной за проверкуClientполномочия.
Хореография такая:
Client.(credentials, serviceID) -> CAS.authRequest
if CAS.check(authRequest) then
CAS.token = genToken(authRequest)
CAS.Success(token) -> Client.result
CAS.Success(token) -> Service.result
else
CAS.Failure -> Client.result
CAS.Failure -> Service.result
Хореография начинается с первой строки, где Client передает пару, состоящую из некоторых учетных данных и идентификатора службы, к которой он хочет получить доступ. CAS. CAS сохраняет эту пару в своей локальной переменной authRequest (для запроса аутентификации).
В строке 2 CAS проверяет, действителен ли запрос для получения токена аутентификации.
Если да, он генерирует токен и передает Success сообщение, содержащее токен для обоих Client и Service (Строки 3–5).
В противном случае CAS информирует Client и Service что аутентификация не удалась, отправив Failure сообщение (строки 7–8). В остальном мы называем эту хореографию «хореографией SSO».
Проекция конечной точки [ править ]
Ключевой особенностью хореографического программирования является возможность компилировать хореографии в распределенные реализации. Эти реализации могут представлять собой библиотеки для программного обеспечения, которое должно участвовать в компьютерной сети, следуя протоколу. [1] [3] [4] или автономные распределенные программы. [5] [6]
Преобразование хореографии в распределенные программы называется проекцией конечной точки (сокращенно EPP). [2] [3]
Проекция конечной точки возвращает программу для каждой роли, описанной в исходной хореографии. [3] Например, учитывая приведенную выше хореографию, проекция конечной точки вернет три программы: одну для Client, один для Serviceи один для CAS. Они показаны ниже в форме псевдокода, где send и recv являются примитивами для отправки и получения сообщений в/из других ролей.
| Клиент | send (credentials, serviceID) to CAS
recv result from CAS
|
|---|---|
| Услуга | recv result from CAS
|
| КАС | recv authRequest from Client
if check(authRequest) then
token = genToken(authRequest)
send Success(token) to Client
send Success(token) to Service
else
send Failure to Client
send Failure to Service
|
Для каждой роли ее код содержит действия, которые роль должна выполнить для правильной реализации хореографии вместе с другими.
Развитие [ править ]
Парадигма хореографического программирования берет свое начало из его титульной кандидатской диссертации. [7] [8] [9] Вдохновение для синтаксиса хореографических языков программирования можно найти в нотации протокола безопасности , также известной как нотация «Алисы и Боба». [1] Хореографическое программирование также находится под сильным влиянием стандартов хореографии обслуживания и диаграмм взаимодействия , а также развития теории исчисления процессов . [1] [3] [10]
Хореографическое программирование – активное направление исследований. Парадигма использовалась при изучении информационных потоков , [11] параллельные вычисления , [12] киберфизические системы , [13] [14] адаптация времени выполнения , [6] и системная интеграция . [15]
Языки [ править ]
- AIOCJ ( веб-сайт ). [6] Хореографический язык программирования для адаптируемых систем , создающий код на языке Джоли .
- Чор ( сайт ). [5] Хореографический язык программирования сеансового типа , который компилируется в микросервисы в Jolie .
- Хоровой ( сайт ). Объектно-ориентированный хореографический язык программирования высшего порядка, который компилируется в библиотеки Java .
- Основная хореография. [16] Основная теоретическая модель хореографического программирования. реализация Механизированная доступна в Coq . [17] [18] [19]
- Вечеринка. [20] Хореографический язык программирования с проверенным компилятором CakeML.
- Пируэт. [8] Теория механизированного хореографического языка программирования с процедурами высшего порядка.
См. также [ править ]
- Обозначение протокола безопасности
- Диаграмма последовательности
- Служебная хореография
- Структурированный параллелизм
- Многоуровневое программирование
Ссылки [ править ]
- ^ Jump up to: Перейти обратно: а б с д и Монтези, Фабрицио (2023). Введение в хореографию . Издательство Кембриджского университета. дои : 10.1017/9781108981491 . ISBN 978-1-108-83376-9 . S2CID 102335067 .
- ^ Jump up to: Перейти обратно: а б с Ёсида, Нобуко; Васконселос, Васко Т.; Падовани, Лука; Боно, Николас Нг; Нейкова, Румяна; Монтези, Фабрицио; Маскарди, Вивиана; Мартинс, Франциско; Йонсен, Эйнар Брох; Ху, Раймонд; Джакино, Елена; Гесберт, Нильс; Гей, Саймон Дж.; Дениелу, Пьер-Мало; Кастанья, Джузеппе; Кампос, Хоана; Молодец, Марио; Боно, Вивиана; Анкона, Давиде (2016). «Типы поведения в языках программирования» . Основы и тенденции в языках программирования . 3 (2–3): 95–230. дои : 10.1561/2500000031 . hdl : 10044/1/44282 .
- ^ Jump up to: Перейти обратно: а б с д и ж Джяллоренцо, Саверио; Монтези, Фабрицио; Пересотти, Марко; Рихтер, Дэвид; Сальванески, Гвидо; Вайзенбургер, Паскаль (2021). Многопартийные языки: хореографические и многоуровневые случаи (Жемчужина) . Международные труды Лейбница по информатике (LIPIcs). Том 194. стр. 22:1–22:27. doi : 10.4230/LIPIcs.ECOOP.2021.22 . ISBN 9783959771900 . (Выдающийся доклад ОКООП 2021)
- ^ Хоровой язык программирования
- ^ Jump up to: Перейти обратно: а б Карбоне, Марко; Монтези, Фабрицио (2013). «Задуманная свобода из тупика» . Материалы 40-го ежегодного симпозиума ACM SIGPLAN-SIGACT по принципам языков программирования — POPL '13 . п. 263. дои : 10.1145/2429069.2429101 . ISBN 9781450318327 . S2CID 15627190 .
- ^ Jump up to: Перейти обратно: а б с Преда, Мила Далла; Габбриелли, Маурицио; Джяллоренцо, Саверио; Ланезе, Иван; Мауро, Якопо (2017). «Динамическая хореография: теория и реализация» . Логические методы в информатике . 13 (2). дои : 10.23638/LMCS-13(2:1)2017 . S2CID 5555662 .
- ^ Монтези, Фабрицио (2013). Хореографическое программирование (PDF) (доктор философии). ИТ-университет Копенгагена. ISBN 978-87-7949-299-8 . (Награда EAPLS за лучшую докторскую диссертацию)
- ^ Jump up to: Перейти обратно: а б Хирш, Эндрю К.; Гарг, Дипак (16 января 2022 г.). «Пируэт: типизированная функциональная хореография высшего порядка» . Труды ACM по языкам программирования . 6 (ПОПЛ): 1–27. arXiv : 2111.03484 . дои : 10.1145/3498684 . S2CID 243833095 . (Выдающийся доклад POPL 2022)
- ^ Аренд Ренсинк (30 августа 2015 г.). «Фабрицио Монтези получает награду EAPLS за лучшую докторскую диссертацию 2014 года» . Европейская ассоциация языков и систем программирования.
- ^ Карбоне, Марко; Хонда, Кохей; Ёсида, Нобуко (2012). «Структурированное коммуникационно-ориентированное программирование для веб-сервисов» . Транзакции ACM в языках и системах программирования . 34 (2): 1–78. дои : 10.1145/2220365.2220367 . S2CID 15737118 .
- ^ Ллуч Лафуэнте, Альберто; Нильсон, Флемминг; Нильсон, Ханне Риис (2015). «Дискретное управление информационными потоками для спецификаций, ориентированных на взаимодействие» . Логика, переписывание и параллелизм (PDF) . Конспекты лекций по информатике. Том. 9200. стр. 427–450. дои : 10.1007/978-3-319-23165-5_20 . ISBN 978-3-319-23164-8 . S2CID 32617923 .
- ^ Крус-Филипе, Луис; Монтези, Фабрицио (2016). «Хореография на практике» . Формальные методы для распределенных объектов, компонентов и систем . Конспекты лекций по информатике. Том. 9688. стр. 114–123. arXiv : 1602.08863 . дои : 10.1007/978-3-319-39570-8_8 . ISBN 978-3-319-39569-2 . S2CID 18067252 .
- ^ Лопес, Уго А.; Хойссен, Кай (2017). «Хореография киберфизических распределенных систем управления для энергетики» . Материалы симпозиума по прикладным вычислениям . стр. 437–443. дои : 10.1145/3019612.3019656 . ISBN 9781450344869 . S2CID 39112346 .
- ^ Лопес, Уго А.; Нильсон, Флемминг; Нильсон, Ханне Риис (2016). «Обеспечение доступности в отказоустойчивых системах связи» (PDF) . Формальные методы для распределенных объектов, компонентов и систем . Конспекты лекций по информатике. Том. 9688. стр. 195–211. дои : 10.1007/978-3-319-39570-8_13 . ISBN 978-3-319-39569-2 . S2CID 12872876 .
- ^ Джяллоренцо, Саверио; Ланезе, Иван; Руссо, Дэниел (2018). «ЧИП: Процесс хореографической интеграции» . На пути к значимым интернет-системам. Конференции OTM 2018 (PDF) . Конспекты лекций по информатике. Том. 11230. стр. 22–40. дои : 10.1007/978-3-030-02671-4_2 . ISBN 978-3-030-02670-7 . S2CID 53015580 .
- ^ Крус-Филипе, Луис; Монтези, Фабрицио (2020). «Базовая модель хореографического программирования» . Теоретическая информатика . 802 : 38–66. arXiv : 1510.03271 . дои : 10.1016/j.tcs.2019.07.005 . S2CID 199122777 .
- ^ Коэн, Лирон; Калишик, Цезарь (2021). Формализация тьюринг-полного хореографического языка в Coq . Международные труды Лейбница по информатике (LIPIcs). Том. 193. стр. 15:1–15:18. doi : 10.4230/LIPIcs.ITP.2021.15 . ISBN 9783959771887 . S2CID 231802115 .
- ^ Кросс-Филип, Луи; Монтези, Фабрицио; Перессотти, Марко (27 мая 2023 г.). «Формальная теория хореографического программирования» . Журнал автоматизированного рассуждения . 67 (2): 21.arXiv : 2209.01886 . дои : 10.1007/ s10817-023-09665-3 ISSN 1573-0670 . S2CID 252090305 .
- ^ Крус-Филипе, Луис; Монтези, Фабрицио; Перессотти, Марко (2021), Чероне, Антонио; Олвечки, Питер Чаба (ред.), «Сертификационный сборник хореографии» , «Теоретические аспекты вычислений - ICTAC 2021» , Конспекты лекций по информатике, том. 12819, Чам: Springer International Publishing, стр. 115–133, arXiv : 2102.10698 , doi : 10.1007/978-3-030-85315-0_8 , ISBN 978-3-030-85314-3 , S2CID 231985665 , получено 7 марта 2022 г.
- ^ Похьола, Йоханнес Оман; Гомес-Лондоньо, Алехандро; Шейкер, Джеймс; Норриш, Майкл (2022). Андроник, июнь; де Моура, Леонардо (ред.). «Калас: проверенный сквозной компилятор хореографического языка» . 13-я Международная конференция по интерактивному доказательству теорем (ITP 2022) . Международные труды Лейбница по информатике (LIPIcs). 237 . Дагштуль, Германия: Замок Дагштуль – Центр информатики Лейбница: 27:1–27:18. дои : 10.4230/LIPIcs.ITP.2022.27 . ISBN 978-3-95977-252-5 . S2CID 251322644 .