Русская Википедия:TLA⁺
TLA+ — язык спецификаций, основанный на теории множеств, логике первого порядка и темпоральной логике действий (Шаблон:Lang-en). Разработан Лесли ЛэмпортомШаблон:Sfn, исследователем теории распределённых систем.
История
Темпоральная логика была введена Амиром Пнуэли в 1970-х годах. Лесли Лэмпорт увидел недостаточность этой идеи для описания систем целиком и пришёл к мысли о необходимости использовать конечные автоматы (Шаблон:Lang-en), которым придавался смысл формул темпоральной логики, описывающих все возможные пути исполнения. Таким образом родилась идея темпоральной логики действий (TLA), которая дополнила темпоральную логику следующим[1]:
- инвариантность при повторении состояния (Шаблон:Lang-en — игра слов state — «состояние» и stuttering — «заикание»),
- темпоральное использование кванторов существования,
- принятие в качестве атомарных формул не только предикатов состояния, но и формул действий.
В результате кропотливой работы над идеями TLA появился язык спецификаций, названный TLA+[1].
Описание
Язык TLA+ несколько схож по духу с Z-нотацией, а возможно даже был создан под её влияниемШаблон:Sfn.
TLA-спецификация — темпоральная формула, часто называемая Spec и являющаяся предикатом (утверждением) о поведении. Поведение представляет собой возможный путь исполнения системы или, другими словами, представлять возможную историю универсума (universe), который может содержать систему. Поведения, удовлетворяющие Spec — правильные поведения системыШаблон:Sfn.
Состоянием называется присваивание значений переменных, шагом называется пара состояний. Теперь поведение можно представить как бесконечную последовательность состояний, а шагами поведения можно назвать пару последовательных состояний поведения. Предикатом состояния называется функция, результат которой — логическое значение истина или ложь — соответствует утверждению о состоянии. Действием называется функция, имеющая смысл предиката над шагом. В этой функции участвуют как переменные первого шага, так и второго, которые обычно отмечаются штрихомШаблон:Sfn.
Одной из простейших нетривиальных спецификаций является следующаяШаблон:Sfn:
- <math>Spec \triangleq Init \land \square [Next]_{(v_1, v_2, \dots, v_n)}</math>
Здесь Init — предикат состояния, Next — действие, vi — переменные, <math>\square</math> — единственный в данной спецификации темпоральный оператор (истинно во всех будущих состояниях).
Примечания
Литература
- 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
- Шаблон:Книга
- Шаблон:Книга
- Lamport L., The temporal logic of actions. ACM Transactions on Programming Languages and Systems, 16(3):872-923, May 1994
- Шаблон:Книга
- Alpern B., Schneider F. B., Defining liveness. Information Processing Letters, 21(4):181-185, October 1985
Шаблон:Свободное и открытое программное обеспечение Microsoft Шаблон:Computer-sci-stub
