TLA⁺

TLA +  este un limbaj de specificație bazat pe teoria mulțimilor , logica de ordinul întâi și logica temporală a acțiunilor ( TLA, logica temporală a acțiunilor ). Dezvoltat de Leslie Lamport [1] , un cercetător în teoria sistemelor distribuite .  

Istorie

Logica temporală a fost introdusă de Amir Pnueli în anii 1970. Leslie Lamport a văzut insuficiența acestei idei pentru a descrie sistemele în ansamblu și a ajuns la ideea necesității de a folosi mașini de stare , cărora  li sa dat semnificația formulelor logice temporale care descriu toate căile de execuție posibile. Astfel, a luat naștere ideea logicii temporale a acțiunilor (TLA), care a completat logica temporală cu următoarele [2] :

• invarianța repetiției  stării _ 
• utilizarea temporală a cuantificatorilor existențiali ,
• acceptând ca formule atomice nu numai predicate de stare, ci şi formule de acţiune.

Ca rezultat al muncii minuțioase asupra ideilor TLA, a apărut un limbaj de specificație numit TLA + [2] .

Descriere

Limbajul TLA + este oarecum similar în spirit cu notația Z și poate chiar să fi fost creat sub influența sa [1] .

O specificație TLA este o formulă temporală, adesea numită Spec, care este un predicat (afirmație) despre comportament . Comportamentul reprezintă o posibilă modalitate de a executa un sistem sau, cu alte cuvinte, reprezintă o posibilă istorie a universului pe care sistemul îl poate conține. Comportamentele care satisfac Spec sunt comportamentele corecte ale sistemului [1] .

O stare este o atribuire de valori variabilelor, un pas este o pereche de stări. Acum , comportamentul poate fi gândit ca o succesiune infinită de stări, iar pașii comportamentului pot fi numiți o pereche de stări succesive ale comportamentului. Un predicat de stare este o funcție al cărei rezultat, valoarea booleană adevărată sau falsă, se potrivește cu declarația de stare. O acțiune este o funcție care are sensul de predicat asupra unui pas. Această funcție implică atât variabilele primului pas, cât și ale celui de-al doilea, care sunt de obicei marcate cu un prim [1] .

Una dintre cele mai simple specificații non-triviale este următoarea [1] :

Aici Init  este un predicat de stare, Next  este o acțiune, v i  sunt variabile,  este singurul operator temporal din această specificație (adevărat în toate stările viitoare).

Note

1. ↑ 1 2 3 4 5 Habrias, Frappier, 2006 , 7.1 Privire de ansamblu asupra TLA+.
2. ↑ 1 2 Leslie Lampport: Limbajul de specificații TLA+ . Consultat la 13 noiembrie 2014. Arhivat din original la 8 martie 2016. (nedefinit)

Literatură

• Amir Pnueli . Logica temporală a programelor. În Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, paginile 46-57. IEEE, noiembrie 1977
• Bjørner, D. și Henson, MC Logics of Specification Languages. - Springer, 2007. - 646 p. — ISBN 9783540741077 .
• Henri Habrias, Marc Frappier. Metode de specificare a software-ului. - John Wiley & Sons, 2006. - 418 p. — ISBN 978-1-905-20934-7 .
• Lampport L. , Logica temporală a acțiunilor. Tranzacții ACM pe limbaje și sisteme de programare, 16(3):872-923, mai 1994
• Lamport, L. Specificarea sistemelor: limbajul și instrumentele TLA+ pentru inginerii hardware și software. - Addison-Wesley, 2003. - 364 p. — ISBN 9780321143068 .
• Alpern B., Schneider FB , Definirea vieții. Information Processing Letters, 21(4):181-185, octombrie 1985