The +CAL Algorithm Language

Last modified 10 July 2006

What is +CAL?

+CAL (pronounced "plus-CAL") is an algorithm language based on TLA+. A +CAL algorithm is translated to a TLA+ specification, which can be checked with the TLC model checker.

An algorithm language is for writing algorithms, just as a programming language is for writing programs. The introduction to the +CAL manual (see below) explains how algorithms differ from programs, and how +CAL differs from programming languages.

New in Version 1.1

Several options have been added with Version 1.1. The two most important are:

You can let the translator add missing labels. In particular, if you omit all labels from a sequential algorithm, then the translator will act as if the necessary labels were there.
There are now two alternate syntaxes: the original, somewhat prolix p-syntax and a new, more compact c-syntax. The c-syntax is closer to that of C-based languages like C# and Java, using braces { and } instead of begin/do and end. There is a separate version of the manual for each syntax; the two syntaxes are briefly compared in both versions.

Obtaining +CAL

Click HERE to download the p-version of the manual.

Click HERE to download the c-version of the manual.

Click HERE to download a TLA+ specification of the +CAL to TLA+ translation.

The +CAL translator is available as part of the TLA+ tool set.

Papers About +CAL

The following papers about +CAL and its use are available:

The +CAL Algorithm Language
Checking a Multithreaded Algorithm with +CAL. (Also see this example.)

The Specification of the Translator

The heart of the +CAL to TLC+ translation is formally formally specified in TLA+ by the file PlusCal.tla, which you can download by clicking HERE. The translator option “-spec PlusCal” causes the TLA+ translation to be produced by having TLC execute this specification on the input. However, this method of performing the translation does not preserve the formatting of expressions, so it does not work if the meaning of an expression depends on proper indentation. Moreover, the resulting TLA+ translation is hard to read.

This page can be found by searching the Web for the 21-letter string uidlamportpluscalhomepage. Please do not put this string in any document that could wind up on the web--including email messages and Postscript and Word documents. You can refer to it in Web documents as "the string obtained by removing the - from uid-lamportpluscalhomepage".