TLA⁺

TLA +  on joukkoteoriaan , ensimmäisen asteen logiikkaan ja toimintojen ajalliseen logiikkaan ( TLA, toimintojen temporaalinen logiikka ) perustuva määrittelykieli . Kehittäjä Leslie Lamport [1] , hajautetun järjestelmän teorian tutkija .  

Historia

Amir Pnueli esitteli ajallisen logiikan 1970-luvulla. Leslie Lamport näki tämän idean riittämättömyyden kuvaamaan järjestelmiä kokonaisuutena ja tuli ajatukseen tilakoneiden käytön tarpeesta , joille  annettiin ajallisen logiikkakaavan merkitys, joka kuvaa kaikkia mahdollisia suorituspolkuja. Näin syntyi ajatus toimien ajallisesta logiikasta (TLA), joka täydensi ajallista logiikkaa seuraavalla [2] :

•  tilan toiston invarianssi _ 
• eksistentiaalisten kvantorien ajallinen käyttö ,
• hyväksymällä atomikaavoja paitsi tilapredikaatteja myös toimintakaavoja.

TLA-ideoita koskevan huolellisen työn tuloksena syntyi määrittelykieli nimeltä TLA + [2] .

Kuvaus

TLA + -kieli on hengeltään jossain määrin samanlainen kuin Z-notaatio , ja se on saatettu jopa syntyä sen vaikutuksen alaisena [1] .

TLA-määritys on ajallinen kaava, jota usein kutsutaan nimellä Spec, joka on predikaatti (lauseke) käyttäytymisestä . Käyttäytyminen edustaa mahdollista tapaa toteuttaa järjestelmä tai toisin sanoen edustaa mahdollista maailmankaikkeuden historiaa, jonka järjestelmä voi sisältää. Specin täyttävä käyttäytyminen on järjestelmän oikeaa käyttäytymistä [1] .

Tila on arvojen määritys muuttujille, askel on tilapari. Nyt käyttäytymistä voidaan ajatella äärettömänä tilojen sarjana, ja käyttäytymisen vaiheita voidaan kutsua käyttäytymisen peräkkäisten tilojen pariksi. Tilapredikaatti on funktio, jonka tulos, boolen arvo tosi tai epätosi, vastaa tilalauseketta. Toiminto on funktio, jolla on askeleen nähden predikaatti. Tämä funktio sisältää sekä ensimmäisen että toisen vaiheen muuttujat, jotka on yleensä merkitty alkuluvulla [1] .

Yksi yksinkertaisimmista ei-triviaalisista spesifikaatioista on seuraava [1] :

Tässä Init  on tilapredikaatti, Next  on toiminta, v i  ovat muuttujia,  on ainoa ajallinen operaattori tässä määrittelyssä (tosi kaikissa tulevissa tiloissa).

Muistiinpanot

1. ↑ 1 2 3 4 5 Habrias, Frappier, 2006 , 7.1 Yleiskatsaus TLA+:sta.
2. ↑ 1 2 Leslie Lamport: Määrittelykieli TLA+ . Haettu 13. marraskuuta 2014. Arkistoitu alkuperäisestä 8. maaliskuuta 2016. (määrätön)

Kirjallisuus

• Amir Pnueli . Ohjelmien ajallinen logiikka. Teoksessa Proceedings of the 18th Annual Symposium on the Funds of Computer Science, sivut 46-57. IEEE, marraskuu 1977
• Bjørner, D. ja Henson, MC Logics of Specification Languages. - Springer, 2007. - 646 s. — ISBN 9783540741077 .
• Henri Habrias, Marc Frappier. Ohjelmiston määrittelymenetelmät. - John Wiley & Sons, 2006. - 418 s. — ISBN 978-1-905-20934-7 .
• Lamport L. , Toimien ajallinen logiikka. ACM Transactions on Programming Languages ​​and Systems, 16(3):872-923, toukokuu 1994
• Lamport, L. Järjestelmät: TLA+-kieli ja työkalut laitteisto- ja ohjelmistosuunnittelijoille. - Addison-Wesley, 2003. - 364 s. — ISBN 9780321143068 .
• Alpern B., Schneider FB , Elävyyden määritteleminen. Information Processing Letters, 21(4):181-185, lokakuu 1985