1;3409;0c The PlusCal Algorithm Language

The PlusCal Algorithm Language

Oretical Aspects of Computing - ICTAC 2009, 6th International Colloquium, vol. 5684, 2009
Pages: 36-60DOI: 10.1007/978-3-642-03466-4_2

International Colloquium on Theoretical Aspects of Computing


Algorithms are different from programs and should not be described with programming languages. The only simple alternative to programming languages has been pseudo-code. PlusCal is an algorithm language that can be used right now to replace pseudo-code, for both sequential and concurrent algorithms. It is based on the TLA +  specification language, and a PlusCal algorithm is automatically translated to a TLA +  specification that can be checked with the TLC model checker and reasoned about formally.