TLA⁺


TLA+ — язык спецификаций, основанный на теории множеств, логике первого порядка и темпоральной логике действий (англ. TLA, temporal logic of actions). Разработан Лесли Лэмпортом, исследователем теории распределённых систем.

История

Темпоральная логика была введена Амиром Пнуэли в 1970-х годах. Лесли Лэмпорт увидел недостаточность этой идеи для описания систем целиком и пришёл к мысли о необходимости использовать конечные автоматы (англ. state machine), которым придавался смысл формул темпоральной логики, описывающих все возможные пути исполнения. Таким образом родилась идея темпоральной логики действий (TLA), которая дополнила темпоральную логику следующим:

  • инвариантность при повторении состояния (англ. stattering — игра слов state — «состояние» и stuttering — «заикание»),
  • темпоральное использование кванторов существования,
  • принятие в качестве атомарных формул не только предикатов состояния, но и формул действий.

В результате кропотливой работы над идеями TLA появился язык спецификаций, названный TLA+.

Описание

Язык TLA+ несколько схож по духу с Z-нотацией, а возможно даже был создан под её влиянием.

TLA-спецификация — темпоральная формула, часто называемая Spec и являющаяся предикатом (утверждением) о поведении. Поведение представляет собой возможный путь исполнения системы или, другими словами, представлять возможную историю универсума (universe), который может содержать систему. Поведения, удовлетворяющие Spec — правильные поведения системы.

Состоянием называется присваивание значений переменных, шагом называется пара состояний. Теперь поведение можно представить как бесконечную последовательность состояний, а шагами поведения можно назвать пару последовательных состояний поведения. Предикатом состояния называется функция, результат которой — логическое значение истина или ложь — соответствует утверждению о состоянии. Действием называется функция, имеющая смысл предиката над шагом. В этой функции участвуют как переменные первого шага, так и второго, которые обычно отмечаются штрихом.

Одной из простейших нетривиальных спецификаций является следующая:

S p e c ≜ I n i t ∧ ◻ [ N e x t ] ( v 1 , v 2 , … , v n ) {displaystyle Spec riangleq Initland square [Next]_{(v_{1},v_{2},dots ,v_{n})}}

Здесь Init — предикат состояния, Next — действие, vi — переменные, ◻ {displaystyle square } — единственный в данной спецификации темпоральный оператор (истинно во всех будущих состояниях).