Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | |||
| learning:pluscal [2025/07/26 17:51] – [C-style vs P-Style] lorinh | learning:pluscal [2025/07/26 17:56] (current) – [Learning Pluscal] lorinh | ||
|---|---|---|---|
| Line 1: | Line 1: | ||
| - | ====== Learning | + | ====== Learning |
| PlusCal is an algorithm language—a language for writing and debugging algorithms. It is especially good for algorithms to be implemented with multi-threaded code. Instead of being compiled into code, a PlusCal algorithm is translated into a TLA+ specification. An algorithm written in PlusCal is debugged using the TLA+ tools—mainly the TLC model checker. Correctness of the algorithm can also be proved with the TLAPS proof system, but that requires a lot of hard work and is seldom done. | PlusCal is an algorithm language—a language for writing and debugging algorithms. It is especially good for algorithms to be implemented with multi-threaded code. Instead of being compiled into code, a PlusCal algorithm is translated into a TLA+ specification. An algorithm written in PlusCal is debugged using the TLA+ tools—mainly the TLC model checker. Correctness of the algorithm can also be proved with the TLAPS proof system, but that requires a lot of hard work and is seldom done. | ||
| - | The easiest way to learn pluscal, is to read the Pluscal tutorial by Lamport. Free, and readable online; it can be found here: https:%%//%%lamport.azurewebsites.net/ | + | ===== External resources ===== |
| + | |||
| + | * [[https:// | ||
| + | * [[https:// | ||
| ===== C-style vs P-Style ===== | ===== C-style vs P-Style ===== | ||
lorinh