From Wikipedia, the free encyclopedia
Jump to: navigation, search

PlusCal (formerly called +CAL) is a formal specification language created by Leslie Lamport, which transpiles to TLA+. In contrast to TLA+'s action-oriented focus on distributed systems, PlusCal most resembles an imperative programming language and is better-suited to specifying sequential algorithms.[1] PlusCal was designed to replace pseudocode, retaining its simplicity while providing a formally-defined and verifiable language.[2] A one-bit clock is written in PlusCal as follows:

-- fair algorithm OneBitClock {
  variable clock \in {0, 1};
    while (TRUE) {
      if (b = 0)
        b := 1
        b := 0    

See also[edit]


  1. ^ Lamport, Leslie (28 February 2015). Principles and Specifications of Concurrent Systems. p. 7. Retrieved 10 May 2015. PlusCal is more convenient than TLA+ for describing the flow of control in an algorithm. This generally makes it better for specifying sequential algorithms and shared-memory multiprocess algorithms. 
  2. ^ Lamport, Leslie (2 January 2009). "The PlusCal Algorithm Language" (PDF). Lecture Notes in Computer Science. Springer Berlin Heidelberg. 5684 (Theoretical Aspects of Computing - ICTAC 2009): 36–60. doi:10.1007/978-3-642-03466-4_2. Retrieved 10 May 2015. 

External Links[edit]