Break It Down

Here's where I break it down, the fundamentals necessary to make a formal specification.

These are prerequisites for understanding how to read and write a formal specification in TLA+.

Propositional Boolean Logic involves the following:

• two Boolean values TRUE and FALSE

• the operators /\ (conjunction), \/ (disjunction)

• negation

• => (implication)

• equivalence.

Set Theory involves the following:

• intersection

• union

• subset

• \ (set difference).

Predicate Logic involves the following:

• universal quantification (for all)

• existential quantification (there exists).

• TLA+ modules are composed of multiple formulas using the mathematical symbols above.

• TLA+ modules should contain a formula, "Spec", which is one formula that defines the whole module.