Временная логика действий
 | Эта статья включает список литературы , связанную литературу или внешние ссылки , но ее источники остаются неясными, поскольку в ней отсутствуют встроенные цитаты . ( январь 2011 г. ) |
Временная логика действий ( TLA ) — это логика, разработанная Лесли Лэмпортом , которая сочетает в себе темпоральную логику с логикой действий .Он используется для описания поведения параллельных и распределенных систем . Это логика, лежащая в основе языка спецификации TLA+ .
Подробности [ править ]
Высказывания во временной логике действий имеют вид , где A — действие, а t содержит подмножество переменных, входящих A. в Действие — это выражение, содержащее переменные со штрихом и без штриха, например . Значение переменных, не отмеченных штрихом, — это значение переменной в этом состоянии . Значение отмеченных переменных — это значение переменной в следующем состоянии .Вышеприведенное выражение означает, что значение x сегодня плюс значение x завтра , умноженное на значение y сегодня , равно значению y завтра .
![{\displaystyle [A]_{t}}](https://wikimedia.org/api/rest_v1/media/math/render/svg/03d6eaf7fc064571a2d2e88332f923d25a436f1c)
Значение заключается в том, что либо A действительно сейчас, либо переменные, входящие в t, не изменяются. Это допускает заикающиеся шаги, на которых ни одна из переменных программы не меняет своих значений.
См. также [ править ]
Ссылки [ править ]
- Лэмпорт, Лесли (2002). Спецификация систем: TLA + Язык и инструменты для инженеров аппаратного и программного обеспечения . Аддисон-Уэсли. ISBN 0-321-14306-Х . Проверено 2 февраля 2007 г.
- Лесли Лэмпорт (16 декабря 1994 г.), Введение в TLA (PDF) , получено 17 сентября 2010 г.
Внешние ссылки [ править ]
- Официальный сайт
- «Система проверки TLA+» . ИНРИА .
- Лэмпорт, Лесли (2014). «Мышление для программистов» .
Нежное введение в TLA+ на выставке Build
 | Эта формальным методам, статья, посвященная незавершена . Вы можете помочь Википедии, расширив ее . |