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

История

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

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

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

Описание

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

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

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

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

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

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

Примечания

Литература

• 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. . — 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