TLA+: Difference between revisions

| authorlinkauthor-link = Leslie Lamport

| publisher = IOS Press,
| location=Amsterdam

| journalseries = NATO Science Series, III: Computer and Systems Sciences

| accessdateaccess-date = 22 May 2015}}

| authorlinkauthor-link = Leslie Lamport

| license = [[MIT License]]<ref name="toolboxlicense">{{cite web

| accessdateaccess-date = 10 May 2015}}

| website = {{URL|research.microsoft.comhttps:/en-us/um/people/lamport.azurewebsites.net/tla/tla.html}}

'''TLA⁺''' is a [[formal specification]] language developed by [[Leslie Lamport]]. It is used tofor designdesigning, modelmodelling, documentdocumentation, and verifyverification of programs, especially [[concurrent systems]] and [[distributed systems]]. TLA⁺ hasis beenconsidered describedto asbe exhaustively-testable [[pseudocode]],<ref name="awsorig">

| lastlast1 = Newcombe

| firstfirst1 = Chris

| accessdateaccess-date = 8 May 2015}}

{{cite journalmagazine

| authorlinkauthor-link = Leslie Lamport

| journalmagazine = Wired

| accessdateaccess-date = 7 May 2015}}

| authorlinkauthor-link = Leslie Lamport

| authorlinkauthor-link = Leslie Lamport

| accessdates2cid = 23 May 2015}}121557270

TLA⁺ was introduced in 1999, following several decades of research into a verification method for concurrent systems. AEver since, a toolchain has sincebeen developed, including an [[interactive development environment|IDE]] and a distributed model checker. The pseudocode-like language [[PlusCal]] was created in 2009; it [[Source-to-source compiler|transpiles]] to TLA⁺ and is useful for specifying sequential algorithms. TLA⁺² was announced in 2014, expanding language support for proof constructs. The current TLA⁺ reference is [http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html The TLA⁺ Hyperbook] by Leslie Lamport.

[[File:Amir Pnueli.jpg|thumb|alt=Portrait of an Israeli man in his sixties. His hair is short and balding, and he is wearing glasses with a dress shirt and jacket.|[[Amir Pnueli]] applied temporal logic to computer science, for which he received the 1996 [[Turing awardAward]].]]

{{quoteblockquote|The usefulness of systems of this sort [on discrete time] does not depend on any serious metaphysical assumption that time is discrete; they are applicable in limited fields of discourse in which we are concerned only with what happens next in a sequence of discrete states, e.g. in the working of a digital computer.}}

| authorlinkauthor-link = Leslie Lamport

| accessdateaccess-date = 22 May 2015}}

| authorlinkauthor-link = Leslie Lamport

| accessdateaccess-date = 22 May 2015}}

| authorlinkauthor-link = Leslie Lamport

| accessdateaccess-date = 22 May 2015}}

{{quoteblockquote|However, I became disillusioned with temporal logic when I saw how Schwartz, Melliar-Smith, and Fritz Vogt were spending days trying to specify a simple [[FIFO (computing and electronics)|FIFO queue]]&nbsp;– arguing over whether the properties they listed were sufficient. I realized that, despite its aesthetic appeal, writing a specification as a conjunction of temporal properties just didn't work in practice.<ref name="lamport-spec"/>}}

| authorlinkauthor-link = Leslie Lamport

| accessdateaccess-date = 22 May 2015}}

| authorlinkauthor-link = Leslie Lamport

| accessdateaccess-date = 22 May 2015}}

| titlechapter = Model checkingChecking TLA⁺ specificationsSpecifications

| accessdateaccess-date = 14 May 2015| series = Lecture Notes in Computer Science

| authorlinkauthor-link = Leslie Lamport

| title = TheTheoretical PlusCalAspects Algorithmof LanguageComputing - ICTAC 2009

| chapter-url = http://research.microsoft.com/en-us/um/people/lamport/pubs/pluscal.pdf

| accessdateaccess-date = 10 May 2015 | isbn = 978-3-642-03465-7

</ref> and the TLA⁺ proof system (TLAPS) in 2012.<ref name="tlaps-survey"/> TLA⁺² was announced in 2014, adding some additional language constructs as well as greatly increasing in-language support for the proof system.<ref name="tla2guide" /> Lamport is engaged in creating an updated TLA⁺ reference, "The TLA⁺ Hyperbook". The incomplete work is [http://research.microsoft.com/en-us/um/people/lamport/tla/hyperbook.html available] from his official website. Lamport is also creating [http://lamport.azurewebsites.net/video/videos.html The TLA⁺ Video Course], described therein as "a work in progress that consists of the beginning of a series of video lectures to teach programmers and software engineers how to write their own TLA⁺ specifications".

| authorlinkauthor-link = Leslie Lamport

| authorlinkauthor-link = Leslie Lamport

TLA⁺ is based on [[Zermelo–Fraenkel set theory|ZF]], so operations on variables involve set manipulation. The language includes set [[Element (mathematics)|membership]], [[Union (set theory)|union]], [[Intersection (set theory)|intersection]], [[Relative complement|difference]], [[powerset]], and [[subset]] operators. [[First-order logic]] operators such as {{math|&or;}}, {{math|&and;}}, {{math|&not;}}, {{math|&rArr;⇒}}, {{math|&harr;↔}}, {{math|&equiv;≡}} are also included, as well as [[universal quantification|universal]] and [[existential quantification|existential]] quantifiers {{math|&forall;}} and {{math|&exist;}}. [[Epsilon calculus|Hilbert's {{math|&epsilon;}}]] is provided as the CHOOSE operator, which uniquely selects an arbitrary set element. Arithmetic operators over [[real number|reals]], [[integers]], and [[natural numbers]] are available from the standard modules.

<nowiki> </nowiki>Temporal existential and universal quantification are included in TLA⁺, although without support from the tools.

The foundational data structure of TLA⁺ is the set. Sets are either explicitly enumerated or constructed from other sets using operators or with <source lang="tex" inlinecode>{x \in S : p}</sourcecode> where ''p'' is some condition on ''x'', or <source lang="tex" inlinecode>{e : x \in S}</sourcecode> where ''e'' is some function of ''x''. The unique [[empty set]] is represented as <code>{}</code>.

| name = TLA⁺ Toolbox

| title = TLA⁺ Toolbox

| latest release version = 1.67.02 Theano

| latest release date = {{Start date and age|20192022|0702|1102}}<!-- {{Start date and age|YYYY|MM|DD|df=yes/no}} -->

| latest preview version = 1.68.10 Clarke

| latest preview date = {{Start date and age|2020|0412|0206}}

| accessdateaccess-date = 14 May 2015}}

</ref> TLAPS has been used to prove correctness of [[Paxos (computer science)#Byzantine Paxos|Byzantine Paxos]], the Memoir security architecture, and components of the [[Pastry (DHT)|Pastry distributed hash table]].,<ref name="tlaps-survey"/> It is distributed separately fromand the restSpire ofconsensus the TLA⁺ tools and is free software, distributed under the [[BSD license]]algorithm.<ref>[https://tla.msr-inria.inria.fr/tlaps/content/Home.html TLA+ Proof System]</refname="spire">{{cite TLA⁺² greatly expanded language support for proof constructs.journal

| accessdateaccess-date = 14 May 2015}}

| authorlink3author-link3 = Leslie Lamport

| title = TLA⁺FM Proofs2012: Formal Methods

| accessdateaccess-date = 14 May 2015| series = Lecture Notes in Computer Science

| title = WhyAbstract AmazonState ChoseMachines, Alloy, B, TLA⁺, VDM, and Z

| journalseries = Lecture Notes in Computer Science

| accessdateaccess-date = 10 May 2017}}

| accessdateaccess-date = 10 May 2017}}

<div class="NavHead">A [[key-value store]] with [[snapshot isolation]]</div>: