Для установки нажмите кнопочку Установить расширение. И это всё.

Исходный код расширения WIKI 2 регулярно проверяется специалистами Mozilla Foundation, Google и Apple. Вы также можете это сделать в любой момент.

4,5
Келли Слэйтон
Мои поздравления с отличным проектом... что за великолепная идея!
Александр Григорьевский
Я использую WIKI 2 каждый день
и почти забыл как выглядит оригинальная Википедия.
Статистика
На русском, статей
Улучшено за 24 ч.
Добавлено за 24 ч.
Альтернативы
Недавние
Show all languages
Что мы делаем. Каждая страница проходит через несколько сотен совершенствующих техник. Совершенно та же Википедия. Только лучше.
.
Лео
Ньютон
Яркие
Мягкие

Из Википедии — свободной энциклопедии

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]:

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

Примечания

  1. 1 2 3 4 5 Habrias, Frappier, 2006, 7.1 Overview of TLA+.
  2. 1 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
Эта страница в последний раз была отредактирована 20 мая 2022 в 01:15.
Как только страница обновилась в Википедии она обновляется в Вики 2.
Обычно почти сразу, изредка в течении часа.
Основа этой страницы находится в Википедии. Текст доступен по лицензии CC BY-SA 3.0 Unported License. Нетекстовые медиаданные доступны под собственными лицензиями. Wikipedia® — зарегистрированный товарный знак организации Wikimedia Foundation, Inc. WIKI 2 является независимой компанией и не аффилирована с Фондом Викимедиа (Wikimedia Foundation).