代码之家 › 专栏 › 技术社区 › Brian Hicks

我如何断言一个数字在TLA+中消失或一个列表在TLA+中成长?

tla+

2

Brian Hicks · 技术社区 · 6 年前

我有一个TLA+规范,我想断言列表的长度只会增长(如果在口吃时保持不变就好了)

NoWorkIsLost == Len(samples) = Len(samples) ~> Len(samples) = Len(samples) + 1

我甚至不知道该在这里搜索什么,我肯定我错过了一些非常明显的东西!

1 回复 | 直到 6 年前

1

2

Hovercouch 6 年前

这取决于你所说的“列表的长度只会增长”是什么意思。最简单的方法就是写

Op == [][Len(samples') > Len(samples)]_Len(samples)

如果长度改变 ,长度必须增加。这仍然允许你在不改变列表的情况下改变列表!如果你改写

Op == [][Len(samples') > Len(samples)]_samples

samples 改变,它的长度也必须增加。但这允许您在一个动作中弹出一个元素并推送两个元素。您可能想表示旧序列是一个新的一个。你可以用它来做

Op == [][SubSeq(samples', 1, Len(samples)) = samples]_samples