PlusCal
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
- TLA+
- Pseudocode
References
- ^ 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.
- ^ 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
- PlusCal tools and documentation are found on the PlusCal Algorithm Language page.
- v
- t
- e
Microsoft Research (MSR)
projects
Languages, compilers |
|
---|---|
Distributed–grid computing |
|
Internet, networking |
|
Other projects | |
Operating systems |
|
APIs |
|
Launched as products |
|
applied
research
Live Labs |
| ||||
---|---|---|---|---|---|
FUSE Labs | |||||
Other labs |
Category
This computer science article is a stub. You can help Wikipedia by expanding it. |
- v
- t
- e