TLA⁺

TLA +  är ett specifikationsspråk baserat på mängdteori , första ordningens logik och temporal logic of actions ( TLA ,  temporal logic of actions ). Utvecklad av Leslie Lamport [1] , en forskare inom teori om distribuerade system .

Historik

Temporal logik introducerades av Amir Pnueli på 1970-talet. Leslie Lamport såg otillräckligheten i denna idé för att beskriva system som helhet och kom till idén om behovet av att använda tillståndsmaskiner , som  gavs innebörden av temporala logiska formler som beskriver alla möjliga exekveringsvägar. Således föddes idén om temporär logik av handlingar (TLA), som kompletterade tidslogik med följande [2] :

•  tillståndsrepetitionsinvarians _ _  _
• temporal användning av existentiella kvantifierare ,
• acceptera som atomformler inte bara tillståndspredikat, utan också handlingsformler.

Som ett resultat av mödosamt arbete med TLA:s idéer dök ett specifikationsspråk kallat TLA + [2] upp .

Beskrivning

TLA + -språket liknar till sin anda något Z-notation , och kan till och med ha skapats under dess inflytande [1] .

En TLA-specifikation är en tidsformel, ofta kallad Spec, som är ett predikat (påstående) om beteende . Beteende representerar ett möjligt sätt att exekvera ett system eller, med andra ord, representerar en möjlig historia av universum som systemet kan innehålla. Beteenden som uppfyller specifikationerna är de korrekta beteendena i systemet [1] .

Ett tillstånd är en tilldelning av värden till variabler, ett steg är ett par tillstånd. Nu kan beteendet ses som en oändlig sekvens av tillstånd, och stegen i beteendet kan kallas ett par på varandra följande tillstånd av beteendet. Ett tillståndspredikat är en funktion vars resultat, det booleska värdet sant eller falskt, matchar tillståndssatsen. En handling är en funktion som har betydelsen av ett predikat över ett steg. Denna funktion involverar både variablerna i det första steget och det andra, som vanligtvis är markerade med ett primtal [1] .

En av de enklaste icke-triviala specifikationerna är följande [1] :

Här är Init  ett tillståndspredikat, Next  är en handling, v i  är variabler,  är den enda temporala operatorn i denna specifikation (sant i alla framtida tillstånd).

Anteckningar

1. ↑ 1 2 3 4 5 Habrias, Frappier, 2006 , 7.1 Översikt över TLA+.
2. ↑ 1 2 Leslie Lamport: Specifikationsspråket TLA+ . Hämtad 13 november 2014. Arkiverad från originalet 8 mars 2016. (obestämd)

Litteratur

• Amir Pnueli . Programmens tidsmässiga logik. I Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, sidorna 46-57. IEEE, november 1977
• Bjørner, D. och Henson, MC Logics of Specification Languages. - Springer, 2007. - 646 sid. — ISBN 9783540741077 .
• Henri Habrias, Marc Frappier. Programvaruspecifikationsmetoder. - John Wiley & Sons, 2006. - 418 sid. — ISBN 978-1-905-20934-7 .
• Lamport L. , Handlingarnas tidslogik. ACM Transactions on Programming Languages ​​and Systems, 16(3):872-923, maj 1994
• Lamport, L. Specificering av system: TLA+-språket och verktygen för maskin- och mjukvaruingenjörer. - Addison-Wesley, 2003. - 364 sid. — ISBN 9780321143068 .
• Alpern B., Schneider FB , Definiera livlighet. Information Processing Letters, 21(4):181-185, oktober 1985