我有一个 TLA+ 规范，我想断言一个列表只会在长度上增长（如果它在口吃时保持不变就很好。）
现在我有这样的事情，但我确定这是不对的：
NoWorkIsLost == Len(samples) = Len(samples) ~> Len(samples) = Len(samples) + 1
我什至不确定要在这里搜索什么，我确定我错过了一些非常明显的东西！
问问题
54 次
1 回答
2
这取决于您所说的“列表只会越来越长”的意思。最简单的方法是写
Op == [][Len(samples') > Len(samples)]_Len(samples)
但这就是说，如果长度发生变化，则长度必须增加。这仍然允许您在不更改列表的情况下更改列表！如果你改为写
Op == [][Len(samples') > Len(samples)]_samples
那么你是说如果samples改变，它也必须增加长度。但这允许您在单个操作中弹出一个元素并推送两个元素。您可能想要表示旧序列是新序列的前缀。你可以这样做
Op == [][SubSeq(samples', 1, Len(samples)) = samples]_samples
于 2019-01-07T03:03:05.750 回答