This is an instruction manual for Version 1.1 of the p-syntax version of the + cal algorithm language. The following section, on page 3, explains the difference between this syntax and the alternative c-syntax. Section 1 explains what an algorithm language is and why you’d want to use one.

Section 2 tells you what you need to know to get started using + cal. After reading it, you’ll be able to write and check + cal algorithms. You can read the other parts of this manual as you need them. The table of contents and the index can help you find what you need. Pages 68–70 at the end, just before the index, contain a series of tables that summarize a lot of useful information. The rest of the manual is arranged in the order you’re likely to want to look at it:

• Section 3 describes the things you’ll find in most programming language manuals, like the statements of the language. Once you’ve started writing + cal algorithms, you should browse this chapter to learn about features of + cal not mentioned in Section 2.
• We run programs, but we check algorithms. Section 2 gets you started using the translator and TLC model checker to check + cal algorithms.
Section 4 tells you more about the translator and TLC. It’s mostly about TLC, describing some of its additional features and how to use it to debug an algorithm. You should go to Section 4 if you don’t understand what the translator or TLC is trying to say when it reports an error.
• Section 5 is mainly about writing
+ cal expressions. The expression language of
+ cal is much richer and more powerful than that of any programming language because it is based on mathematics, not on programming. The ten or so pages about expressions in Section 5 just introduce the subject. You can learn more from the book Specifying Systems, referred to here as the TLA + book [2], or from any books on the elementary mathematics of sets, functions, and logic—especially ones written by mathematicians and not computer scientists.
• Section A of the appendix contains a BNF grammar of + cal. The subjects of Appendix Sections B and C will make no sense to you until you’ve read Section 1. Don’t forget about the table of contents, the tables on pages 68–70, and the index

Download pdf A + CAL User’s Manual P-Syntax Version