TLA⁺

TLA +  er et specifikationssprog baseret på mængdeteori , førsteordenslogik og handlingslogik ( TLA ,  handlingslogik ). Udviklet af Leslie Lamport [1] , en forsker i teori om distribuerede systemer .

Historie

Temporal logik blev introduceret af Amir Pnueli i 1970'erne. Leslie Lamport så utilstrækkeligheden af ​​denne idé til at beskrive systemer som en helhed og kom til ideen om behovet for at bruge statsmaskiner , som  fik betydningen af ​​tidsmæssige logiske formler, der beskriver alle mulige udførelsesveje. Således blev ideen om temporær logik af handlinger (TLA) født, som supplerede tidslogik med følgende [2] :

•  tilstand gentagelse invarians _ 
• tidsmæssig brug af eksistentielle kvantifikatorer ,
• at acceptere som atomformler ikke kun statsprædikater, men også handlingsformler.

Som et resultat af omhyggeligt arbejde med ideerne om TLA dukkede et specifikationssprog kaldet TLA + [2] op .

Beskrivelse

TLA + -sproget minder i ånden noget om Z-notation og kan endda være blevet skabt under dets indflydelse [1] .

En TLA-specifikation er en tidsmæssig formel, ofte kaldet Spec, der er et prædikat (udsagn) om adfærd . Adfærd repræsenterer en mulig måde at eksekvere et system på eller repræsenterer med andre ord en mulig historie af universet, som systemet kan indeholde. Adfærd, der opfylder specifikationerne, er den korrekte adfærd i systemet [1] .

En tilstand er en tildeling af værdier til variable, et trin er et par tilstande. Nu kan adfærden opfattes som en uendelig sekvens af tilstande, og trinene i adfærden kan kaldes et par på hinanden følgende tilstande af adfærden. Et tilstandsprædikat er en funktion, hvis resultat, den boolske værdi sand eller falsk, matcher tilstandssætningen. En handling er en funktion, der har betydningen af ​​et prædikat over et trin. Denne funktion involverer både variablerne i det første trin og det andet, som normalt er markeret med et primtal [1] .

En af de enkleste ikke-trivielle specifikationer er følgende [1] :

Her er Init  et tilstandsprædikat, Next  er en handling, v i  er variable,  er den eneste tidsmæssige operator i denne specifikation (sand i alle fremtidige tilstande).

Noter

1. ↑ 1 2 3 4 5 Habrias, Frappier, 2006 , 7.1 Oversigt over TLA+.
2. ↑ 1 2 Leslie Lamport: Specifikationssproget TLA+ . Hentet 13. november 2014. Arkiveret fra originalen 8. marts 2016. (ubestemt)

Litteratur

• Amir Pnueli . Programmers tidsmæssige logik. I Proceedings of the 18th Annual Symposium on the Foundations of Computer Science, side 46-57. IEEE, november 1977
• Bjørner, D. og Henson, MC Logics of Specification Languages. - Springer, 2007. - 646 s. — ISBN 9783540741077 .
• Henri Habrias, Marc Frappier. Softwarespecifikationsmetoder. - John Wiley & Sons, 2006. - 418 s. — ISBN 978-1-905-20934-7 .
• Lamport L. , Handlingers tidsmæssige logik. ACM Transactions on Programming Languages ​​and Systems, 16(3):872-923, maj 1994
• Lamport, L. Angivelse af systemer: TLA+-sproget og værktøjerne til hardware- og softwareingeniører. - Addison-Wesley, 2003. - 364 s. — ISBN 9780321143068 .
• Alpern B., Schneider FB , Definition af livlighed. Information Processing Letters, 21(4):181-185, oktober 1985