creating:start

Differences

This shows you the differences between two versions of the page.

Link to this comparison view

Both sides previous revision Previous revision
Next revision		 Previous revision
creating:start [2025/03/29 13:54] – Changed start link to scanning page ahelwercreating:start [2025/04/01 14:46] (current) – Expanded and reordered language feature list ahelwer
Line 19: Line 19:
 And, if you reach the edge of those capabilities - well, you're well-placed to extend TLC to handle it! And, if you reach the edge of those capabilities - well, you're well-placed to extend TLC to handle it!
  
-===== Getting Started =====+===== Overview =====
  
 This tutorial uses Java. This tutorial uses Java.
Line 33: Line 33:
 Future expansions will cover liveness checking and, possibly, proof checking. Future expansions will cover liveness checking and, possibly, proof checking.
 A minimal subset of the TLA⁺ language is used; users are encouraged to extend their tools to handle additional TLA⁺ syntax as desired. A minimal subset of the TLA⁺ language is used; users are encouraged to extend their tools to handle additional TLA⁺ syntax as desired.
 +
 +===== The Language =====
 +
 +TLA⁺ is a large, complicated, and ambiguous language that takes a huge amount of work to parse correctly & completely.
 +This is assisted by [[https://github.com/tlaplus/rfcs/tree/2a772d9dd11acec5d7dedf30abfab91a49de48b8/language_standard/tests/tlaplus_syntax|a comprehensive test corpus]] exercising the language's nooks & crannies, but here we will make life easy on ourselves.
 +This tutorial only uses a minimal subset of TLA⁺ syntax, enough to handle [[https://github.com/tlaplus/Examples/blob/37236893f14527b4fc9f3963891eb2316c3de62e/specifications/DieHard/DieHarder.tla|the generalized DieHard spec]] with some inconvenience.
 +While that may seem limiting, this tutorial tries to focus on the difficult & interesting parts of bringing TLA⁺ to life instead of more mundane drudgework like handling all hundred-some user-definable operator symbols.
 +You are encouraged to extend this minimal core as you wish; language tooling is best developed incrementally!
 +Slowly filling in the details of this rough language sketch has a satisfying meditative aspect.
 +
 +Here is what our minimal language subset includes:
 +  * Whole natural numbers like ''0'', ''5'', ''10'', etc.
 +  * Boolean values ''TRUE'' and ''FALSE''
 +  * Finite set literals, like ''{1, 2, 3, 4, 5}''
 +  * Parentheses for expression grouping
 +  * ''IF''/''THEN''/''ELSE'' expressions
 +  * Single-line comments like ''\* comment text''
 +  * The ''ENABLED'', negative (''-''), and logical negation (''~'') prefix operators
 +  * Some infix operators: ''\in'', ''='', ''+'', ''-'', ''..'', ''/\'', ''\/'', and ''<''
 +  * The variable-priming suffix operator
 +  * Quantification over sets with ''\E'' and ''\A''
 +  * Function construction and application, like ''[e \in S |-> op(e)]'' and ''f[e]''
 +  * Named operator definitions like ''op == ...'' and ''op(x, y, z) == ...''
 +  * Declaration of ''VARIABLES''
 +  * Vertically-aligned conjunction & disjunction lists
 +
 +Notably, we do not use the familiar ''---- MODULE Name ----''/''===='' encapsulation.
 +Files simply consist of a series of unit-level TLA⁺ definitions.
 +We also do not leave room for a separate model configuration file; all ''CONSTANT'' values must instead be hardcoded, and well-known names like ''Init'', ''Next'', ''TypeOK'', and ''Inv'' identify important definitions.
 +
 +As outlined above, you are free to add missing features (or even your own invented features!) as you wish.
 +Each chapter ends with a set of challenges that often involve adding these missing features.
 +
 +===== Getting Started =====
 +
 +Read part I (the first three chapters) of free online textbook //[[https://craftinginterpreters.com/contents.html|Crafting Interpreters]]// by Robert Nystrom.
 +We will be closely following the material in this book, modifying it to our uses.
 +The first two chapters are a nice introduction and overview of language implementation generally.
 +Chapter three specifies a toy language called Lox, to be used as an object of study for the remainder of the book.
 +Our minimal TLA⁺ subset has some similarity to Lox with regard to expressions involving integers and booleans, but also differences - you can skip the section on closures (unless you want to implement higher-order operator parameters yourself) and the section on classes.
 +What's important is that it's similar enough for all the fundamentals to still apply!
 +
 +Code snippets are shown often in this tutorial.
 +When a snippet is similar to code given in the book with the exception of a few lines, the differing lines will be highlighted.
 +For example:
 +<code java [highlight_lines_extra="2"]>
 +  private char advance() {
 +    column++;
 +    return source.charAt(current++);
 +  }
 +</code>
 +
 +Highlighting is also used to identify //new// code being added to a large section of code given previously, with line numbers and surrounding lines included for context.
 +For example:
 +<code java [enable_line_numbers="true",highlight_lines_extra="2",start_line_numbers_at=82]>
 +      case '\n':
 +        column = 0;
 +        line++;
 +        break;
 +</code>
 +
 +Sometimes the code given here is so different from that provided by the book that highlighting is simply ommitted to reduce visual noise.
 +A parenthetical will specify the meaning of highlighted code when ambiguous.
  
 To begin the tutorial, start at page [[creating:scanning|Scanning TLA⁺ Tokens]]. To begin the tutorial, start at page [[creating:scanning|Scanning TLA⁺ Tokens]].
 +
  • creating/start.1743256446.txt.gz
  • Last modified: 2025/03/29 13:54
  • by ahelwer