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
In computer science, pseudocode is a plain language description of the steps in an algorithm or another system. Pseudocode often uses structural conventions of a normal programming language, but is intended for human reading rather than machine re ...
, retaining its simplicity while providing a formally-defined and verifiable language.
[
] A
one-bit clock is written in PlusCal as follows:
-- fair algorithm OneBitClock
See also
*
TLA+
*
Pseudocode
In computer science, pseudocode is a plain language description of the steps in an algorithm or another system. Pseudocode often uses structural conventions of a normal programming language, but is intended for human reading rather than machine re ...
References
External links
* PlusCal tools and documentation are found on th
PlusCal Algorithm Language page
Formal methods
Formal specification languages
Algorithm description languages
Microsoft Research
{{Comp-sci-stub