Skip to Main content Skip to Navigation

Auxiliary Variables in TLA+

Leslie Lamport 1 Stephan Merz 2, 3
2 VERIDIS - Modeling and Verification of Distributed Algorithms and Systems
MPII - Max-Planck-Institut für Informatik, Inria Nancy - Grand Est, LORIA - FM - Department of Formal Methods
3 MOSEL - Proof-oriented development of computer-based systems
LORIA - FM - Department of Formal Methods
Abstract : Auxiliary variables are often needed for verifying that an implementation is correct with respect to a higher-level specification. They augment the formal description of the implementation without changing its semantics–that is, the set of behaviors that it describes. This paper explains rules for adding history, prophecy, and stuttering variables to TLA+ specifications, ensuring that the augmented specification is equivalent to the original one. The rules are explained with toy examples, and they are used to verify the correctness of a simplified version of a snapshot algorithm due to Afek et al.
Document type :
Complete list of metadata

Cited literature [9 references]  Display  Hide  Download
Contributor : Stephan Merz Connect in order to contact the contributor
Submitted on : Sunday, May 28, 2017 - 2:19:04 PM
Last modification on : Wednesday, November 3, 2021 - 7:57:30 AM
Long-term archiving on: : Wednesday, September 6, 2017 - 10:36:25 AM


Files produced by the author(s)


  • HAL Id : hal-01488617, version 2
  • ARXIV : 1703.05121



Leslie Lamport, Stephan Merz. Auxiliary Variables in TLA+. [Research Report] Inria Nancy - Grand Est (Villers-lès-Nancy, France); Microsoft Research. 2017. ⟨hal-01488617v2⟩



Les métriques sont temporairement indisponibles