PlusCal (formerly called +CAL) is a formal specification language created by
Leslie Lamport
Leslie B. Lamport (born February 7, 1941 in Brooklyn) is an American computer scientist and mathematician. Lamport is best known for his seminal work in distributed systems, and as the initial developer of the document preparation system LaTeX an ...
, which
transpiles to
TLA+. In contrast to TLA
+'s
action-oriented focus on
distributed systems
A distributed system is a system whose components are located on different networked computers, which communicate and coordinate their actions by passing messages to one another from any system. Distributed computing is a field of computer sci ...
, PlusCal most resembles an
imperative programming
In computer science, imperative programming is a programming paradigm of software that uses statements that change a program's state. In much the same way that the imperative mood in natural languages expresses commands, an imperative program ...
language and is better-suited when specifying
sequential algorithm In computer science, a sequential algorithm or serial algorithm is an algorithm that is executed sequentially – once through, from start to finish, without other processing executing – as opposed to concurrently or in parallel. The term is prim ...
s.
[
] 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:
-- fair algorithm OneBitClock
See also
*
TLA+
*
Pseudocode
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