PlusCal

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 when specifying sequential algorithms. PlusCal was designed to replace pseudocode, retaining its simplicity while providing a formally defined and verifiable language. A one-bit clock is written in PlusCal as follows:

Formal specification language created by Leslie Lamport

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 when 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 (clock = 0)
        clock := 1
      else 
        clock := 0    
    }
  }
}

See also

[edit]

• FizzBee
• TLA⁺
• Pseudocode

References

[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). Theoretical Aspects of Computing - ICTAC 2009. Lecture Notes in Computer Science. Vol. 5684. Springer Berlin Heidelberg. pp. 36–60. doi:10.1007/978-3-642-03466-4_2. ISBN 978-3-642-03465-7. Retrieved 10 May 2015.

External links

[edit]

• PlusCal tools and documentation are found on the PlusCal Algorithm Language page.

This computer science article is a stub. You can help Wikipedia by adding missing information.

• v
• t
• e