TLA⁺

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

История

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

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

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

Описание

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

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

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

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

${\displaystyle Spec\triangleq Init\land \square [Next]_{(v_{1},v_{2},\dots ,v_{n})}}$

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

Примечания

1. Habrias, Frappier, 2006, 7.1 Overview of TLA+.
2. Leslie Lamport: The Specification Language TLA+  (неопр.). Дата обращения: 13 ноября 2014. Архивировано 8 марта 2016 года.

Литература

• Amir Pnueli. The temporal logic of programs. In Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, pages 46-57. IEEE, November 1977
• Bjørner, D. and Henson, M.C. Logics of Specification Languages. — Springer, 2007. — 646 p. — ISBN 9783540741077.
• Henri Habrias, Marc Frappier. Software Specification Methods. — John Wiley & Sons, 2006. — 418 p. — ISBN 978-1-905-20934-7.
• Lamport L., The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994
• Lamport, L. Specifying Systems: The TLA+ Language and Tools for Hardware and Software Engineers. — Addison-Wesley, 2003. — 364 p. — ISBN 9780321143068.
• Alpern B., Schneider F. B., Defining liveness. Information Processing Letters, 21(4):181-185, October 1985