TLA+
TLA+ — формальна мова специфікації, розроблена Леслі Лампортом і використовується для проектування, моделювання, документування й перевірки програм, особливо розподілених систем. TLA+ описана як вичерпно перевірений псевдокод, і її використання подібне до креслення; TLA є англійською абревіатурою для часової логіки дій.
Що стосується дизайну та документації, TLA + виконує ту саму мету, що й неофіційні технічні умови. Однак специфікації TLA+ написані мовою логіки та математики, і точність специфікацій, написаних цією мовою, призначена для виявлення вад дизайну до початку впровадження системи.
Оскільки специфікації TLA + написані офіційною мовою, вони піддаються перевірці з обмеженою моделлю. Модель перевірки знаходить усі можливі поведінки системи до деякої кількості етапів виконання та вивчає їх на порушення бажаних властивостей інваріантності, таких як безпека та життєздатність. Технічні характеристики TLA+ використовують базову теорію множин для визначення безпеки та часову логіку для визначення життєдіяльності.
TLA+ також використовується для написання перевірених машиною доказів правильності як алгоритмів, так і математичних теорем. Докази написані в декларативному, ієрархічному стилі, незалежному від теореми. Як формальні, так і неофіційні структуровані математичні докази можуть бути записані у TLA+; мова схожа на LaTeX, і існують інструменти для перекладу специфікацій TLA+ до документів LaTeX.
TLA+ була введена в 1999 році, після кількох десятиліть досліджень методу верифікації для одночасних систем. З тих пір було розроблено ланцюжок інструментів, що включає IDE та розподілену перевірку моделей. TLA+2 було оголошено у 2014 році, розширивши мовну підтримку для конструкцій із підтвердженням.
- ↑ Лампорт, Леслі (січень 2000). Specifying Concurrent Systems with TLA+ (PDF). Т. 173, № Calculational System Design. IOS Press, Амстердам. с. 183—247. ISBN 978-90-5199-459-9. Архів оригіналу (PDF) за 4 березня 2016. Процитовано 22 травень 2015.
{{cite book}}
: Проігноровано|journal=
(довідка) - ↑ Tlaplus Tools - License. CodePlex. Microsoft, Compaq. 8 квітня 2013. Процитовано 10 травня 2015.[недоступне посилання] https://tlaplus.codeplex.com/license[недоступне посилання]
На цю статтю не посилаються інші статті Вікіпедії. Будь ласка розставте посилання відповідно до прийнятих рекомендацій. |