Определение систем: язык и инструменты TLA+
Книга «Определение систем: язык и инструменты TLA+ для разработчиков аппаратного и программного обеспечения»
https://lamport.azurewebsites.net/tla/book.html
(можно скачать)
Specifying Systems
Leslie Lamport
--
TLA+ — язык спецификаций, основанный на теории множеств, логике первого порядка и темпоральной логике действий (англ. TLA, temporal logic of actions). Разработан Лесли Лэмпортом[1], исследователем теории распределённых систем.
https://ru.wikipedia.org/wiki/TLA⁺
--
Введение [скрыть]
https://lamport.azurewebsites.net/tla/high-level-view.html
TLA+ — это язык для моделирования программного обеспечения выше уровня кода и аппаратного обеспечения выше уровня схемы.
У него есть IDE (интегрированная среда разработки) для написания моделей и запуска инструментов для их проверки. Инструмент, наиболее часто используемый инженерами, — это средство проверки моделей TLC, но есть также средство проверки доказательств. TLA+ основан на математике и не похож ни на один язык программирования. Большинство инженеров сочтут PlusCal, описанную ниже, самым простым способом начать использовать TLA+.
Модели TLA+ обычно называют спецификациями. В этом введении они называются моделями.
--
Книга
Книга состоит из 364 страниц (включая 17-страничный индекс). Однако большинству людей захочется прочитать только первую часть, состоящую из первых семи глав и занимающую 83 страницы. Вот список глав.
Немного простой математики
Указание простых часов
Асинхронный интерфейс
ФИФО
Кэширующая память
Еще немного математики
Написание спецификации: несколько советов
Живучесть и справедливость
Реальное время
Составление спецификаций
Расширенные примеры
Синтаксический анализатор
Наборщик текста TLAtex
Средство проверки моделей TLC
Синтаксис TLA+
Операторы TLA+
Значение модуля
Стандартные модули
===
ps
Язык TLA+ несколько схож по духу с Z-нотацией, а возможно даже был создан под её влиянием[1].
https://ru.wikipedia.org/wiki/Z-нотация
Z — нотация, основанная на модели
https://deep-econom.livejournal.com/1014910.html
https://lamport.azurewebsites.net/tla/book.html
(можно скачать)
Specifying Systems
Leslie Lamport
--
TLA+ — язык спецификаций, основанный на теории множеств, логике первого порядка и темпоральной логике действий (англ. TLA, temporal logic of actions). Разработан Лесли Лэмпортом[1], исследователем теории распределённых систем.
https://ru.wikipedia.org/wiki/TLA⁺
--
Введение [скрыть]
https://lamport.azurewebsites.net/tla/high-level-view.html
TLA+ — это язык для моделирования программного обеспечения выше уровня кода и аппаратного обеспечения выше уровня схемы.
У него есть IDE (интегрированная среда разработки) для написания моделей и запуска инструментов для их проверки. Инструмент, наиболее часто используемый инженерами, — это средство проверки моделей TLC, но есть также средство проверки доказательств. TLA+ основан на математике и не похож ни на один язык программирования. Большинство инженеров сочтут PlusCal, описанную ниже, самым простым способом начать использовать TLA+.
Модели TLA+ обычно называют спецификациями. В этом введении они называются моделями.
--
Книга
Книга состоит из 364 страниц (включая 17-страничный индекс). Однако большинству людей захочется прочитать только первую часть, состоящую из первых семи глав и занимающую 83 страницы. Вот список глав.
Немного простой математики
Указание простых часов
Асинхронный интерфейс
ФИФО
Кэширующая память
Еще немного математики
Написание спецификации: несколько советов
Живучесть и справедливость
Реальное время
Составление спецификаций
Расширенные примеры
Синтаксический анализатор
Наборщик текста TLAtex
Средство проверки моделей TLC
Синтаксис TLA+
Операторы TLA+
Значение модуля
Стандартные модули
===
ps
Язык TLA+ несколько схож по духу с Z-нотацией, а возможно даже был создан под её влиянием[1].
https://ru.wikipedia.org/wiki/Z-нотация
Z — нотация, основанная на модели
https://deep-econom.livejournal.com/1014910.html