TLA⁺

TLA +  je specifikační jazyk založený na teorii množin , logice prvního řádu a časové logice akcí ( TLA, temporal logic of actions )  . Vyvinutý Leslie Lamport [1] , výzkumník v teorii distribuovaných systémů .

Historie

Temporální logiku zavedl Amir Pnueli v 70. letech 20. století. Leslie Lamport viděl nedostatečnost tohoto nápadu pro popis systémů jako celku a dospěl k myšlence potřeby používat stavové automaty , které  dostaly význam vzorců časové logiky, které popisují všechny možné cesty provádění. Tak se zrodila myšlenka časové logiky akcí (TLA), která časovou logiku doplnila o následující [2] :

• neměnnost opakování  stavu _ 
• dočasné použití existenciálních kvantifikátorů ,
• přijímat za atomické formule nejen stavové predikáty, ale i akční formule.

V důsledku usilovné práce na myšlenkách TLA se objevil jazyk specifikace nazvaný TLA + [2] .

Popis

Jazyk TLA + je svým duchem poněkud podobný Z-notaci a možná dokonce vznikl pod jeho vlivem [1] .

Specifikace TLA je dočasný vzorec, často nazývaný Spec, který je predikátem (výrokem) o chování . Chování představuje možný způsob provedení systému nebo jinými slovy představuje možnou historii vesmíru, kterou systém může obsahovat. Chování vyhovující Spec jsou správné chování systému [1] .

Stav je přiřazení hodnot proměnným, krok je dvojice stavů. Nyní lze chování považovat za nekonečnou posloupnost stavů a ​​kroky chování lze nazvat dvojicí po sobě jdoucích stavů chování. Predikát stavu je funkce, jejíž výsledek, booleovská hodnota true nebo false, odpovídá příkazu stavu. Akce je funkce, která má význam predikátu nad krokem. Tato funkce zahrnuje jak proměnné prvního kroku, tak i druhého, které jsou obvykle označeny prvočíslem [1] .

Jedna z nejjednodušších netriviálních specifikací je následující [1] :

Zde Init  je predikát stavu, Next  je akce, v i  jsou proměnné,  je jediným časovým operátorem v této specifikaci (pravda ve všech budoucích stavech).

Poznámky

1. ↑ 1 2 3 4 5 Habrias, Frappier, 2006 , 7.1 Přehled TLA+.
2. ↑ 1 2 Leslie Lamport: Jazyk specifikace TLA+ . Získáno 13. listopadu 2014. Archivováno z originálu 8. března 2016. (neurčitý)

Literatura

• Amir Pnueli . Časová logika programů. In Sborník příspěvků z 18. výročního sympozia o základech informatiky, strany 46-57. IEEE, listopad 1977
• Bjørner, D. a Henson, MC Logics of Specification Languages. - Springer, 2007. - 646 s. — ISBN 9783540741077 .
• Henri Habrias, Marc Frappier. Metody specifikace softwaru. - John Wiley & Sons, 2006. - 418 s. — ISBN 978-1-905-20934-7 .
• Lamport L. , Časová logika jednání. ACM Transactions on Programming Languages ​​and Systems, 16(3):872-923, květen 1994
• Lamport, L. Specifikace systémů: Jazyk a nástroje TLA+ pro hardwarové a softwarové inženýry. - Addison-Wesley, 2003. - 364 s. — ISBN 9780321143068 .
• Alpern B., Schneider FB , Definice živosti. Information Processing Letters, 21 (4): 181-185, říjen 1985