Auxiliary Variables in TLA+
Logic in Computer Science
2017-05-30 v2
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.
Cite
@article{arxiv.1703.05121,
title = {Auxiliary Variables in TLA+},
author = {Leslie Lamport and Stephan Merz},
journal= {arXiv preprint arXiv:1703.05121},
year = {2017}
}