Временная логика действий

Логика, используемая для описания поведения параллельных систем.

Временная логика действий ( TLA ) — это логика, разработанная Лесли Лэмпортом , которая объединяет временную логику с логикой действий . Она используется для описания поведения параллельных и распределенных систем . Это логика, лежащая в основе языка спецификаций TLA+ .

Подробности

Выражения во временной логике действий имеют вид , где A — действие, а t содержит подмножество переменных, появляющихся в A . Действие — это выражение, содержащее переменные со штрихами и без штрихов, например . Значение переменных без штрихов — это значение переменной в этом состоянии . Значение переменных со штрихами — это значение переменной в следующем состоянии . Выражение выше означает, что значение x сегодня плюс значение x завтра , умноженное на значение y сегодня , равно значению y завтра . ${\displaystyle [A]_{t}}$ ${\displaystyle x+x'*y=y'}$

Значение в том, что либо A теперь допустимо, либо переменные, появляющиеся в t, не изменяются. Это допускает прерывистые шаги, в которых ни одна из переменных программы не изменяет свои значения. ${\displaystyle [A]_{t}}$

Языки спецификации

Существует несколько языков спецификации, реализующих временную логику действий. Каждый язык имеет уникальные особенности и варианты использования:

ТЛА+

TLA+ — это язык спецификации по умолчанию и наиболее широко используемый для TLA. Это математический язык, разработанный для описания поведения параллельных и распределенных систем. Спецификация написана в функциональном стиле.

----------------------------- МОДУЛЬ HourClock -----------------------------РАСШИРЯЕТ НатуральныеПЕРЕМЕННЫЕ часИнициализация == час = 1Следующий == час' = ЕСЛИ час = 12 ТО 1 ИНАЧЕ час + 1Spec == Init /\ [][Next]_hour=============================================== ==========================

PlusCal

PlusCal — это язык алгоритмов высокого уровня, который транслируется в TLA+. Он позволяет пользователям писать алгоритмы в знакомом синтаксисе, похожем на псевдокод, который затем автоматически преобразуется в спецификации TLA+. Это делает PlusCal идеальным для тех, кто предпочитает мыслить в терминах алгоритмов, а не конечных автоматов.

----------------------------- МОДУЛЬ HourClock ----------------------РАСШИРЯЕТ Натуральные(*--алгоритм HourClock { переменная час = 1; { в то время как (ИСТИНА) { час := (час % 12) + 1; } }} --*)

Квинт

Quint — еще один язык спецификации, который транслируется в TLA+. Quint сочетает в себе надежную теоретическую базу временной логики действий (TLA) с современными инструментами проверки типов и разработки. В отличие от PlusCal, операторы и ключевые слова Quint имеют однозначный трансляцию в TLA+.

Физзби

FizzBee ^[1] — это язык спецификации более высокого уровня, использующий синтаксис, подобный синтаксису Python, разработанный для внедрения формальных методов для основных инженеров-программистов, работающих над распределенными системами. Хотя он основан на временной логике действий, он не транслируется в TLA+ и не использует его под капотом, в отличие от PlusCal или Quint.

Действие  Инициализация :  час  =  1атомарное  действие  Tick :  # Тело действий — Starlark (диалект Python)  час  =  ( час  %  12 )  +  1

Смотрите также

• Временная логика
• PlusCal
• ТЛА+

Ссылки

1. "Самый простой язык формальных методов для разработчиков, создающих распределенные системы, микросервисы и облачные приложения" . Получено 28 мая 2024 г.

• Лампорт, Лесли (2002). Спецификация систем: язык и инструменты TLA+ для инженеров аппаратного и программного обеспечения. Addison-Wesley. ISBN 0-321-14306-X.
• Лесли Лэмпорт (16 декабря 1994 г.), Введение в TLA (PDF) , получено 17 сентября 2010 г.
• «Самый простой язык формальных методов для разработчиков, создающих распределенные системы, микросервисы и облачные приложения» . Получено 28 мая 2024 г.

Внешние ссылки

• Официальный сайт
• «Система доказательств TLA+». INRIA .
• Лампорт, Лесли (2014). "Thinking for Programmers". Небольшое введение в TLA+ на Build
• «Сайт FizzBee».
• «Git-репозиторий Quint».