Просмотр кода страницы TLA⁺

'''TLA<sup>+</sup>''' — [[язык спецификаций]], основанный на [[Теория множеств|теории множеств]], [[Логика первого порядка|логике первого порядка]] и [[Темпоральная логика|темпоральной логике]] действий ({{lang-en|TLA, temporal logic of actions}}). Разработан [[Лэмпорт, Лесли|Лесли Лэмпортом]]{{sfn|Habrias, Frappier|2006|loc=7.1 Overview of TLA+}}, исследователем [[Распределённые вычисления|теории распределённых систем]].

== История ==
[[Темпоральная логика]] была введена [[Пнуэли, Амир|Амиром Пнуэли]] в 1970-х годах. Лесли Лэмпорт увидел недостаточность этой идеи для описания систем целиком и пришёл к мысли о необходимости использовать конечные автоматы ({{lang-en|state machine}}), которым придавался смысл формул темпоральной логики, описывающих все возможные пути исполнения. Таким образом родилась идея темпоральной логики действий (TLA), которая дополнила темпоральную логику следующим<ref name="Leslie Lamport">{{Cite web |url=http://research.microsoft.com/en-us/um/people/lamport/pubs/commentary-web.pdf |title=Leslie Lamport: The Specification Language TLA+ |access-date=2014-11-13 |archive-date=2016-03-08 |archive-url=https://web.archive.org/web/20160308052844/http://research.microsoft.com/en-us/um/people/lamport/pubs/commentary-web.pdf |deadlink=no }}</ref>:
* инвариантность при повторении состояния ({{lang-en|stattering}} — игра слов state — «состояние» и stuttering — «заикание»),
* темпоральное использование [[Квантор существования|кванторов существования]],
* принятие в качестве атомарных формул не только предикатов состояния, но и формул действий.

В результате кропотливой работы над идеями TLA появился язык спецификаций, названный TLA<sup>+</sup><ref name="Leslie Lamport" />.

== Описание ==
Язык TLA<sup>+</sup> несколько схож по духу с [[Z-нотация|Z-нотацией]], а возможно даже был создан под её влиянием{{sfn|Habrias, Frappier|2006|loc=7.1 Overview of TLA+}}.

TLA-спецификация — темпоральная формула, часто называемая Spec и являющаяся предикатом (утверждением) о ''поведении''. Поведение представляет собой возможный путь исполнения системы или, другими словами, представлять возможную историю универсума (universe), который может содержать систему. Поведения, удовлетворяющие Spec — правильные поведения системы{{sfn|Habrias, Frappier|2006|loc=7.1 Overview of TLA+}}.

''Состоянием'' называется присваивание значений переменных, ''шагом'' называется пара состояний. Теперь ''поведение'' можно представить как бесконечную последовательность состояний, а ''шагами поведения'' можно назвать пару последовательных состояний поведения. ''Предикатом состояния'' называется функция, результат которой — логическое значение истина или ложь — соответствует утверждению о состоянии. ''Действием'' называется функция, имеющая смысл предиката над шагом. В этой функции участвуют как переменные первого шага, так и второго, которые обычно отмечаются штрихом{{sfn|Habrias, Frappier|2006|loc=7.1 Overview of TLA+}}.

Одной из простейших нетривиальных спецификаций является следующая{{sfn|Habrias, Frappier|2006|loc=7.1 Overview of TLA+}}:

: <math>Spec \triangleq Init \land \square [Next]_{(v_1, v_2, \dots, v_n)}</math>

Здесь ''Init'' — предикат состояния, ''Next'' — действие, ''v<sub>i</sub>'' — переменные, <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
* {{книга
 | автор         = Bjørner, D. and Henson, M.C.
 | заглавие      = Logics of Specification Languages
 | издательство  = Springer
 | год           = 2007
 | allpages      = 646
 | isbn          = 9783540741077
 | ref           = Bjørner, Henson
}}
* {{книга
|автор=Henri Habrias, Marc Frappier
|часть = 
|заглавие=Software Specification Methods
|ссылка=https://archive.org/details/softwarespecific0000unse_b0c1
|издательство=John Wiley & Sons
|год=2006
|allpages=418
|isbn=978-1-905-20934-7
|ref=Habrias, Frappier
}}
* ''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
 | allpages      = 364
 | isbn          = 9780321143068
 | ref           = Lamport — Specifying Systems
}}
* ''Alpern B., Schneider F. B.'', Defining liveness. Information Processing Letters, 21(4):181-185, October 1985
{{Свободное и открытое программное обеспечение Microsoft}}
{{computer-sci-stub}}
[[Категория:Языки спецификаций]]
[[Категория:Формальные методы]]