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

Question

我有一个规范，试图定义一个LRU缓存系统，而我遇到的问题之一是如何从结构键/值配对(基本上是字典或其他语言的散列映射)中删除值。

以下是目前为止的规范本身(不完整)：

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

我参考了这是关于学习TLA Plus的文档。网站，但似乎没有从列表中删除键值对的任何内容。到目前为止，我唯一能想到的是过滤出匹配键的值，并创建一个新的字典对象，但是我更喜欢一个更直接访问的方法。

Answer 1

在我回答之前，我必须问另一个问题：“删除一个值”是什么意思？记住，TLA+不是一种编程语言:它是一种规范语言。这意味着它建立在对你所做的事情有一个非常清楚的理解的基础上。所以让我们来谈谈删除。

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

相应的动作是取序列的尾部。Lamport在http://lamport.azurewebsites.net/tla/book-02-08-08.pdf的第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模块中使用)

在这一点上，它的味道可能是我们走错了方向，可能有一种更简单的方式来指定一个不断变化的dict。我猜您的规范并不依赖于键的某些实现细节:如果您使用字符串而不是整数作为键，则不会期望缓存更改行为。在这种情况下，我会指定一组任意的键和值，这样我们就可以像这样定义突变：

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突变这个词。