2

我有一个规范，我试图定义一个 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

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

4

2 回答 2

7

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

TLA+ 中仅有的两个复杂集合是集合和函数。函数将一组元素（其域）映射到值。结构和序列只是函数的语法糖：结构的域是它的固定键，而序列的域是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 模块中）

在这一点上，它可能尝起来好像我们走错了路，可能有一种更简单的方法来指定一个不断变化的 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]

Wheredict[key] = NULL表示该键不在字典中。

这通常是我向初学者推荐 PlusCal 的原因之一，因为这样您就不必担心如何在学习规范的基础知识时改变函数。如果你正在编写一个 pluscal 算法，你可以用dict[key] := val.

于 2017-11-05T05:38:32.830 回答
2

添加到@Hovercouch 的答案：与编程语言不同，“删除”不符合 TLA+ 规范的含义。

声明dictionary为 aVARIABLE表示它是不带参数（ nullarydictionary ）的运算符的标识符，并且可以根据行为（“随着时间”）更改值。它没有说别的。

查看步骤（行为中的一对连续状态），dictionary（在第一个状态中）的值和dictionary'（dictionary在第二个状态中的）的值是不相关的 [1, p.313]。只有通过规范中表达的约束，我们才能限制它们的值。

如果处于 state dictionary = [x \in {"foo", "bar"} |-> x]，则dictionary'可以是任何东西（ZF中的任何值，即任何集合）。见[1，秒。第 72 页，第 6.5 节。“不要……”在第 80 页，第 139--140 页]。

状态谓词的值

dictionary["foo"] = "foo"

在这种状态下TRUE，因为确实dictionary将值映射"foo"到值"foo"。相反，状态谓词：

dictionary["foo"] = "bar"

是FALSE，因为"foo" # "bar"。如果在以该状态为第一个状态的步骤中，我们编写（另见 [1, p.82]）：

(dictionary["foo"] = "foo")'

我们只是说表达式在下一个状态中dictionary["foo"]等于。我们没有说那是那个状态下的函数——只是说它是一个恰好等于 equal的值。也许那里没有功能。"foo"dictionarydictionary["foo"]"foo"dictionary

什么是函数？

我们什么时候将给定的值f称为“函数”？答案是f恰好满足公式IsAFunction(f)，其中运算符IsAFunction定义为 [1, p.303]：

IsAFunction(g) == g = [x \in DOMAIN g |-> g[x]]

元组（“数组”）是1..n一些具有域的函数n \in Nat。在 TLA+ 中，函数只是具有上述属性的值。由于 ZF 中的任何值都是一个集合，因此函数也是集合，因为我们仍然可以写y \in fwhen fis a function [1, above Sec. 第 43 页的第 4.5 节和第 30 页的第 3.3 节]。

例如，使用定理证明器TLAPS，我们可以证明以下定理并使用Isabelle通过运行来检查证明tlapm -v -C test.tla：

---- MODULE test ----
EXTENDS TLAPS

f == [x \in {} |-> x]
g == [x \in {1, 2} |-> 3]

THEOREM
    LET
        S == f \cup {g}
    IN
        (1 \in f) => (1 \in S)
    PROOF BY Zenon
    (* you can replace this with OBVIOUS *)
=====================

（模型检查器TLC枚举状态，并且由于我们不知道恰好是函数的集合中包含哪些元素，因此 TLC 无法评估表达式y \in f，从而引发Error: Attempted to check if the value: ... is an element of the function .... 句法分析器SANY确认上述模块很好-形成。）

我们也可以写f[x]when fis not a function 或 when x \notin DOMAIN f。问题是在这些情况下，值f[x]是未指定的，因此规范不应取决于这些值是什么。

对规范的评论

该表达式dictionary = []不是 TLA+ 的一部分。要编写具有空域的函数（只有一个这样的函数，请参阅关于函数可扩展性的公理 [1, p.303]）：

dictionary = [x \in {} |-> TRUE]

我将声明capacity为 a CONSTANT，因为它旨在对行为保持不变（当然，除非它发生变化）。此外，currentSize规范并没有减少，但我认为这还没有被添加。

还值得注意的是，dictionary将每个项目映射到一个唯一的值，而queue最终可以包含同一项目的多个副本。不确定 OP 对这种情况有何打算。

EXTENDS Integers, Sequences


CONSTANT capacity
VARIABLES currentSize, queue, dictionary


Init == /\ (capacity = 3 ) /\ (currentSize = 0)
        /\ (queue = <<>>) /\ (dictionary = [x \in {} |-> TRUE])

AddItem(Item, Value) ==
    IF currentSize < capacity

        (* Overwrite to what value the dictionary maps
        the value. *)
        THEN /\ currentSize' = currentSize + 1
             /\ queue' = Append(queue, Item)
             /\ dictionary' =
                     [x \in DOMAIN dictionary |->
                         IF x = Item
                             THEN Value
                             ELSE dictionary[x]]

        (* Remove the leading item from the dictionary's domain,
        then add the given item (perhaps the same), and
        map it to the given value. *)
        ELSE /\ queue' = Append(Tail(queue), Item) 
             /\ LET
                   (* It can happen that OldDom = NewDom. *)
                   OldDom == DOMAIN queue
                   first == queue[1]
                   TailDom == OldDom \ { first }
                   NewDom == TailDom \cup {Item}
                IN
                   dictionary' =
                       [x \in NewDom |->
                           IF x = Item
                               THEN Value
                               ELSE dictionary[x]]

GetItem(Item) == dictionary[item]

Next == \/ AddItem 
        \/ GetItem

表达方式

dictionary' = [x \in DOMAIN dictionary |->
               IF x = Item THEN Value ELSE dictionary[x]]

可以替换为 [1, p.49]

dictionary' = [dictionary EXCEPT ![Item] = Value]

表达方式

dictionary' = [x \in NewDom |->
               IF x = Item THEN Value ELSE dictionary[x]]

不能替换为EXCEPT。

参考

[1] Leslie Lamport，“指定系统”，Addison-Wesley，2002

于 2017-11-05T16:38:17.237 回答