A High-Level Language for Modeling Algorithms and Their Properties - Formal Methods: Foundations and Applications - page 57

verification of liveness properties. We have already mentioned (weak) fairness
annotations for processes in section 3.1; these ensure that whenever a process
instance is continually executable, it will eventually proceed. A strongly fair
process is guaranteed to make progress if it is repeatedly (though not necessarily
continually) executable. PlusCal also supports fairness annotations attached to
individual statements (i.e., labels) rather than to entire processes. For example,
the leading “ + ” signs decorating the labels enter , crit ,and exit indicate weak
fairness assumptions for the corresponding statements.

3.3 The PlusCal Compiler

The basic idea of the translation of PlusCal to TLA + is to represent each group
of statements between two labels, and hence executed atomically, by a TLA +
action formula. (An action formula contains unprimed and primed copies of state
variables, which represent the values of these variables before and after the state
transition.) Control flow is made explicit by adding a variable containing the
values of the program counters of all process instances and of the main program
(if present). Technically, the PlusCal compiler proceeds in three phases, as
illustrated in Fig. 3.

Parser. The PlusCal parser is generated from a JavaCC grammar. Besides
analyzing the algorithm for syntactic errors, the parser also constructs a symbol
table, maintaining information about declared identifiers and checking that their
use respects the scoping rules. This phase generates an abstract syntax tree
(AST) that represents the PlusCal algorithm.

Translation to intermediate format. For clarity and modularity, we split the
compilation into two phases. The first phase makes the control flow explicit and
converts the AST to a list of labeled guarded commands ( branch statements)
whose branches contain only assignments. Each branch ends with an explicit
assignment to the program counter of the entity executing the statements. For
example, the statement

λ : while P
do B

μ : ...

end while

ν : ...

(where there are no labels within the group of statements B ) would first generate
the guarded command

λ : branch

P

then B ;pc[self]:= μ ;

P then pc[self] := ν ;
end branch

¬