在集合上迭代

K. Rustan M. Leino Manuscript KRML 275, 17 February 2020

摘要 以确定的方式处理集合或映射的内容需要一些工作。通过一个典型的例子，本文说明了一种方法。

数学集合类型包括集合、多集、序列和映射。这些对于规范和程序都是必不可少的。在这样的集合的元素上定义函数比人们想象的要困难(或者至少需要更多的劳动)。在本文中，我开发了一个将映射转换为成对序列的示例的程序和证明。该工作的核心部分涉及获得一个可编译函数，该函数以可预测的顺序返回集合的元素。

本文的目标是生成可编译函数。

0. 映射到序列

映射是键值对的集合，其中没有键重复。我们可以将一个map转换为一个序列，方法是将它的键放入一个序列中，然后通过获取每个键的值来生成对:

function method MapToSequence<A,B>(m: map<A,B>): seq<(A,B)> {
  var keys := SetToSequence(m.Keys);
  seq(|keys|, i requires 0 <= i < |keys| => (keys[i], m[keys[i]]))
}

function method SetToSequence<A>(s: set<A>): seq<A>
  ensures var q := SetToSequence(s);
    forall i :: 0 <= i < |q| ==> q[i] in s

对于map m，表达式m。“Keys”表示一组钥匙。函数 MapToSequence 将这组键传递给 SetToSequence `以获得这些键的序列。然后，序列构造函数

seq(n, f)

生成一个长度为n的序列，其中索引i的元素被指定为f(i)。在MapToSequence中，序列推导式的第二个参数是由lambda表达式给出的部分函数

i requires 0 <= i < |keys| => (keys[i], m[keys[i]])

对于给定范围内的索引，该函数返回由键keys[i]和对应的值m组成的对。必须在函数的前提条件中给出i的范围，否则表达式keys[i]将导致下标错误。

为了避免表达式m[keys[i]]中的key-is-not-in-map错误，我们需要知道keys[i]是m的一个键。这需要我们知道他们之间的联系。key 和 Keys ，这是在(尚未实现)函数 SetToSequence `的后置条件中声明的。

我们现在需要实现SetToSequence。

1. 虚函数

让我们从简单的开始。我们将SetToSequence定义为一个虚函数。定义是递归的。当给定的集合非空时，该函数使用choose操作符，也就是let-such-that操作符，并写入:|，从集合中选取一个元素。

function SetToSequence<A>(s: set<A>): seq<A>
  ensures var q := SetToSequence(s);
    forall i :: 0 <= i < |q| ==> q[i] in s
{
  if s == {} then [] else
    var x :| x in s;
    [x] + SetToSequence(s - {x})
}

那不算太坏

2. 编译函数

为了使我们上面写的SetToSequence可编译，我们将关键字function更改为关键字短语function method。这将生成一个错误消息:

如果要使>可编译，则let-such-that表达式的值必须唯一确定

在Dafny中，表达式和函数(其主体是表达式)必须是确定性的。这意味着

var x :| x in s;

当给定相同的s时，总是需要为x取相同的值。这将在运行时进行计算，因此Dafny将这个负担交给了程序员(参见[0 (opens new window)])。

一种方法是强化条件x in s，让它总是从s中选取最小值。这将唯一地确定let-such-that表达式的值。但是“最小值”是什么意思呢?我们从已知最小值的整数开始，然后求一般情况。

3. 选择最小的整数

现在，我们只关注整数集。这让我们加强了let-such-that表达式中的条件，从而唯一地讨论集合中的最小元素:

function method SetToSequence(s: set<int>): seq<int>
  ensures var q := SetToSequence(s);
    forall i :: 0 <= i < |q| ==> q[i] in s
{
  if s == {} then [] else
    var x :| x in s && forall y :: y in s ==> x <= y;
    [x] + SetToSequence(s - {x})
}

“唯一确定的”需求现在得到了满足。然而，由于我们新的such-that谓词更加复杂，验证器提出了一个不同的抱怨:

不能建立满足该谓词的LHS值的存在性

对我们来说，一个非空集合有一个最小元素似乎很清楚，但我们需要说服验证者。让我们用一个单独的引理来做这个，我们声明如下:

lemma ThereIsAMinimum(s: set<int>)
  requires s != {}
  ensures exists x :: x in s && forall y :: y in s ==> x <= y

我们将在SetToSequence中的let-such表达式之前插入对这个引理的调用。这样，函数体就变成了

if s == {} then [] else
  ThereIsAMinimum(s);
  var x :| x in s && forall y :: y in s ==> x <= y;
  [x] + SetToSequence(s - {x})

4. 证明存在最小值

我们的下一个任务是证明“存在最小”引理。下面是一个注释证明:

lemma ThereIsAMinimum(s: set<int>)
  requires s != {}
  ensures exists x :: x in s && forall y :: y in s ==> x <= y
{
  var x :| x in s;
  if s == {x} {
    // obviously, x is the minimum
  } else {
    // The minimum in s might be x, or it might be the minimum
    // in s - {x}. If we knew the minimum of the latter, then
    // we could compare the two.
    // Let`s start by giving a name to the smaller set:
    var s` := s - {x};
    // So, s is the union of s` and {x}:
    assert s == s` + {x};
    // The following lemma call establishes that there is a
    // minimum in s`.
    ThereIsAMinimum(s`);
  }
}

证明从从s中选取任意元素x开始。如果它是s中唯一的元素，它就是最小值。否则，这个证明引出了s是s + {x} `的事实。对引理的递归调用，通过它的后置条件，告诉我们在s中存在一个最小元素。验证器会自动提供剩余的验证胶，这样我们就完成了。

证明中的断言可能看起来很愚蠢。我们只是定义s为s - {x}。因为x在s中，所以属性s == s + {x} 紧跟其后。是的,确实。验证者可以很容易地确认这一点，但验证者没有足够的创造力来意识到这是一个值得了解的好属性。这是处理集合时的典型情况。例如，如果你正在处理一个序列 q ，你可以单独考虑 q[0] ，并对 q[1..] `进行递归调用。如果是这样，您可能需要手动供应

assert [q[0]] + q[1..] == q;

与set属性一样，验证器很容易证明这个属性，但它自己不会想到它。

这个证明的寓意是，当你将一个集合分割成更小的块，你想要分别进行推理时，断言整个集合等于更小块的组合是一个好主意。

5. 总命令

上面对整数集的限制很好用，因为整数集的最小值很容易定义，并且给出唯一的元素。要对其他类型应用相同的技巧，我们还需要能够为这些类型定义一个“最小值”。为了定义最小值，你需要一个“总顺序”。让我们回顾一下这是什么意思。

类型A上的关系是一个函数(A, A) -> bool。当满足以下三个条件时，这种关系称为“R”，称为“偏序”:

• R是自反的，也就是说， forall a:: R(a, a) -“R”是反对称的，即 forall a, b:: R(a, b) && R(b, a) ==> a == b -“R”是可传递的，即 的原则,a, b, c:: R (a, b) & & (b, c) = = > R (a, c) `

A total order是另外满足以下条件的部分order:

-“R”是连接(紧密连接)，即: forall a, b:: R(a, b) || R(b, a)

请注意，连接意味着自反性。

下面是一个谓词，它表示一个给定的关系是否是一个完整的顺序:

predicate IsTotalOrder<A(!new)>(R: (A, A) -> bool) {
  // connexity
  && (forall a, b :: R(a, b) || R(b, a))
  // antisymmetry
  && (forall a, b :: R(a, b) && R(b, a) ==> a == b)
  // transitivity
  && (forall a, b, c :: R(a, b) && R(b, c) ==> R(a, c))
}

Dafny不允许我们在谓词中写这些量词，除非它对类型“a”有更多的了解。如果A是一个类类型，那么在Dafny中的forall意味着量化类A的分配实例。这意味着分配另一个“A”实例可能会导致“IsTotalOrder(R)”更改值。为了防止这种情况的发生，Dafny坚持认为，无限制的量化，如“IsTotalOrder”中的那些，应该在不依赖于分配状态的类型上。我们用类型特征 (!new)来表示，它被写成类型参数声明中类型名的后缀。

6. 通用集合为序列

我们修改了SetToSequence，也取了一个关系R，我们要求它是一个完整的顺序。在此过程中，我们将整数的总顺序<=更改为R，并将R作为参数添加到thereisminimum引理中:

function method SetToSequence<A(!new)>(s: set<A>, R: (A, A) -> bool): seq<A>
  requires IsTotalOrder(R)
  ensures var q := SetToSequence(s, R);
    forall i :: 0 <= i < |q| ==> q[i] in s
{
  if s == {} then [] else
    ThereIsAMinimum(s, R);
    var x :| x in s && forall y :: y in s ==> R(x, y);
    [x] + SetToSequence(s - {x}, R)
}

lemma ThereIsAMinimum<A(!new)>(s: set<A>, R: (A, A) -> bool)
  requires s != {} && IsTotalOrder(R)
  ensures exists x :: x in s && forall y :: y in s ==> R(x, y)

修改后的“SetToSequence”引理进行验证。我们剩下的任务是证明这个引理。

7. 总命令有最小值

我们开始证明泛型的thereisminimum，类似于上面对整数集的证明:

{
  var x :| x in s;
  if s == {x} {  // error: postcondition might not hold on this return path
  } else {
  }
}

以前“显而易见”的情况这次却给验证者带来了麻烦。让我们帮助它。我们的证明义务是证明s中的某个元素和s中的任何一个元素一样小。如果s是单集{x}，那么我们要寻找的元素只能是x。现在，如果y是s中的元素，我们需要证明R(x, y)因为s是一个单例，所以我们有y == x，然后R(x, y)紧跟着连通性。验证者丢失了这两个事实中的一个。让我们对第一个事实添加一个断言:

  if s == {x} {
    assert forall y :: y in s ==> x == y;

啊，是的，验证者可以证明这个断言，然后可以进行剩下的证明。

再来看看非单例情况。我们将像上面的整数集证明一样开始:

  } else {
    var s` := s - {x};
    assert s == s` + {x};
    ThereIsAMinimum(s`, R);

验证者抱怨引理的后置条件可能不成立，所以我们将给验证者更多的帮助。

对引理的递归调用(顺便说一下，这个引理被称为“归纳假说”)表明，在s中存在一个最小值。让我们给它一个名字，我们通过引入一个局部变量来约束它的值，以满足引理的后置条件存在量词中的条件:

    var z :| z in s` && forall y :: y in s` ==> R(z, y);

因为s是s + {x} ，所以我们要寻找的最小值要么是 z ，要么是 x `。让我们分别对待这些情况。我们用“if”语句来实现这一点。由于这两种情况是如此对称，我认为使用Dafny的if-case语句看起来很好:

    // by connexity, one of the two cases below applies
    if
    case R(z, x) =>
      // prove z is the minimum not just of s`, but of s
      // ...
    case R(x, z) =>
      // prove x is the minimum of s
      // ...

我们先来看R(z, x)的情况。最难的部分可能是后置条件中的量词，所以让我们从它开始。要证明一个全称量词，可以使用“forall”语句。

      forall y | y in s
        ensures R(z, y)
      {

从y in s，我们知道要么y是x要么y是s。对于前者，证明是基于守卫的R(z, x)。对于后者，证明来自于我们用来引入“z”的这种条件下的量化。不知何故，验证者没有注意到这一点，所以让我们帮助它。我们从这里开始:

        assert x == y || y in s`;
      }

你瞧!这就是验证者所需要的。

在R(x, z)的情况下，我们将给出类似的forall命题来证明引理的后置条件中的量词:

      forall y | y in s
        ensures R(x, y)
      {

如果y是x，则R(x, y)紧跟在连通性后面。另一方面，如果y在s中，那么引入z的那个条件告诉我们R(z, y)所以我们通过传递性得到R(x, y)你可以用不同的方式添加这些提示，使证明更加有效。这里有一种方法:

        assert y in s` ==> R(z, y);
      }

最后一个评论。当我们证明整数集的最小值时，我认为包含这样的断言通常是有用的:

    assert s == s` + {x};

我也把它包含在通用的“thereisminimum”中。但事实证明，它实际上并不需要(因为我们在两种情况下提供的额外提示中弥补了它)，所以如果你愿意，你可以删除它。

8. 返回映射到序列

我们做到了!

在我们宣布成功之前，让我们确保我们能使用我们的函数和引理来写MapToSequence函数，我们要写的函数。下面是通用版本，它需要一个给定的总顺序:

function method MapToSequence<A(!new),B>(m: map<A,B>, R: (A, A) -> bool): seq<(A,B)>
  requires IsTotalOrder(R)
{
  var keys := SetToSequence(m.Keys, (a,a`) => R(a, a`));
  seq(|keys|, i requires 0 <= i < |keys| => (keys[i], m[keys[i]]))
}

我们也可以将它专门化为整数集:

function method IntMapToSequence<B>(m: map<int,B>): seq<(int,B)> {
  MapToSequence(m, (a, a`) => a <= a`)
}

我们做到了

9. 结论

我希望这段漫长的旅程向您展示了在Dafny处理藏品的一两件事。

参考文献

[0]K. Rustan M. Leino. Compiling Hilbert`s epsilon operator. In Ansgar Fehnker, Annabelle McIver, Geoff Sutcliffe, and Andrei Voronkov, editors, LPAR-20. 20th International Conferences on Logic for Programming, Artificial Intelligence and Reasoning — Short Presentations, volume 35 of EPiC Series in Computing, pages 106–118. EasyChair, 2015. 🔎 (opens new window)