TLA +：如何删除结构键/值对？

Question

我有一个规范试图在其中定义LRU Cache系统，而我遇到的问题之一就是如何从结构键/值对（基本上是字典或哈希表）中删除值其他语言）。

这是到目前为止的规范本身（不完整）：

EXTENDS Integers, Sequences
VARIABLES capacity, currentSize, queue, dictionary

Init == /\ (capacity = 3 ) /\ (currentSize = 0)
        /\ (queue = <<>>) /\ (dictionary = [])


AddItem(Item, Value) == IF currentSize < capacity
            THEN /\ currentSize' = currentSize + 1
                 /\ queue' = Append(queue, Item)
                 /\ dictionary[item] = value
            ELSE /\ queue' = Append(Tail(queue), Item) 
                 /\ dictionary' = [x \in dictionary: x /= queue[3]]

GetItem(Item) == dictionary[item]

Next == \/ AddItem 
        \/ GetItem

我在Learn TLA Plus网站上引用了此文档，但是从列表中删除键值对似乎没有任何帮助。到目前为止，我唯一想做的就是过滤出与键匹配的值并创建一个新的字典对象，但是我更喜欢直接访问更多的方法。

Answer 1

在我回答之前，我必须问另一个问题：“删除值”是什么意思？请记住，TLA +不是编程语言：它是规范语言。这意味着它基于对您正在做的事情的非常清晰的了解。因此，让我们谈谈删除。

TLA +中仅有的两个复杂集合是集合和函数。函数将某些元素集（其domain）映射到值。结构和序列是刚刚超过功能语法糖：一个结构的结构域是其固定键，而序列的结构域是1..n，n \in Nat。函数需要有一个域。如果要从结构中“删除”密钥，则需要从结构的域中“删除”它。

相应的动作是采取序列的尾部。Lamport在“ 指定系统”的第341页上定义了该名称，该名称包含在TLA +工具箱中。这是定义（来自标准模块Sequences.tla-在链接版本中稍有修改）：

Tail(seq) == [i \in 1 .. (Len(seq) - 1) |-> seq[i + 1]]

换句话说，序列的尾部是通过将序列偏移一个偏移量而删除最后一个元素来定义的。通过构造相同的函数，从函数的域中删除某些内容是“完成”的，而在其域中没有该元素。当您考虑它时，这是有道理的：我们只能对数字7进行变异，而不能对数学函数进行变异。

再一次，我们需要在现有功能的基础上构造新功能，以使TLA +添加一些方便的语法。为了更改函数中的单个映射，我们有EXCEPT。为了添加新的映射，TLC模块添加了@@运算符。人们通常不会删除映射，因此我们必须自己定义它。你必须做类似的事情

dictionary' = [x \in DOMAIN dictionary \ {item} |-> dictionary[x]]

请注意，您添加到字典的方式是错误的：dictionary[item] = value是相等检查，而不是赋值。dictionary'[item] = value也不起作用，因为它没有完全指定dictionary。你必须做类似的事情

dictionary' = [x \in {item} |-> value] @@ dictionary

（或:>在TLC模块中也使用）

在这一点上，可能会感觉我们走错了路，也许有一种更简单的方法来指定变化的字典。我猜您的规范并不取决于键的某些实现细节：如果您使用字符串而不是整数作为键，则您不希望缓存更改行为。在这种情况下，我将指定任意一组键和值，这使我们可以定义如下所示的突变：

CONSTANTS Keys, Values, NULL
VARIABLE dict \* [key \in Keys |-> NULL]

Add(dict, key, val) == [dict EXCEPT ![key] = val]
Del(dict, key, val) == [dict EXCEPT ![key] = NULL]

其中dict[key] = NULL表示该键不在词典中。

这通常是我向初学者推荐PlusCal的原因之一，因为那样您就不必在学习规范基础时就担心如何对函数进行突变。如果您要编写加法算法，则可以使用来使字典变异dict[key] := val。