TLA+ 中的辅助变量
计算机科学中的逻辑
2017-05-30 v2
摘要
在验证实现相对于高层规约的正确性时，通常需要使用辅助变量。它们在不改变实现语义（即它所描述的行为集合）的情况下扩充了实现的形式描述。本文解释了向 TLA+ 规约中添加历史变量、预言变量和卡顿变量的规则，确保扩充后的规约与原始规约等价。这些规则通过玩具示例进行了解释，并用于验证 Afek 等人提出的快照算法简化版本的正确性。
引用
@article{arxiv.1703.05121,
title = {Auxiliary Variables in TLA+},
author = {Leslie Lamport and Stephan Merz},
journal= {arXiv preprint arXiv:1703.05121},
year = {2017}
}