Recursive Operator Definitions

Définitions récursives d’opérateurs

Georges Gonthier (1) , Leslie Lamport (2)

1 SPECFUN - Symbolic Special Functions : Fast and Certified
2 Microsoft Research

TLA+ originally allowed recursive function definitions, but not recursive operator definitions, because it was not known how how to define their semantics. They were added to the language in 2006 after we discovered a semantics for them. We describe that semantics here.

Initialement, TLA+ autorisait les définitions récursives de fonctions, mais pas d’opérateurs, car la sémantique à donner à de telles définitions n’était pas claire. Elles furent finalement ajoutées au langage de spécification en 2006, lorsque nous avons découvert un moyen de leur donner une sémantique satisfaisante. Ce rapport décrit cette sémantique.

Mots clés: logic; formal methods; specification; TLA

Mots clés: logique; méthodes formelles; spécification; TLA

Domaines: Théorie et langage formel [cs.FL]; Logique en informatique [cs.LO]

Georges Gonthier, Leslie Lamport. Recursive Operator Definitions. [Research Report] RR-9341, Inria Saclay Ile de France. 2020, pp.17. ⟨hal-02598330⟩