集合元素上的函数

K. Rustan M. Leino Manuscript KRML 274, 16 February 2020

摘要 在自然语言中，像“一组数字的和”这样的短语很容易说和理解。在正式设置中定义和使用这些函数需要更多的工作。这个问题与递归定义的函数如何从集合中选取下一个元素有关。本文描述了一个具有代表性的例子，并描述了如何使正式的繁文缛节发挥作用。该解可应用于集合上的任何交换运算和结合运算。

对集合的元素求和

假设我们有一个函数，它返回集合中所有整数的和:

function Sum(s: set<int>): int

如果我们把一个元素y加到一个集合中，我们期望它的和增加y。也就是说，我们希望正确实现以下方法:

method AddElement(s: set<int>, a: int, y: int) returns (t: set<int>, b: int)
  requires a == Sum(s) && y !in s
  ensures t == s + {x} && b == Sum(t)
{
  t := s + {y};
  b := a + y;
}

事实证明，证明不是自动的。让我们看看细节并填写证明。

求和的递归定义

函数“Sum”是递归定义的。空集合的和为0。如果集合非空，选择其中一个元素，比如x。然后，在递归计算的剩余元素的和上加上x。

function Sum(s: set<int>): int {
  if s == {} then 0 else
    var x := Pick(s);
    x + Sum(s - {x})
}

这个定义使用了一个函数Pick，它返回给定集合中的任意元素。以下是它的定义:

function Pick(s: set<int>): int
  requires s != {}
{
  var x :| x in s; x
}

我待会再讲Pick。此时您需要了解的是，Pick的调用者无法控制返回s中的哪个元素。

不合格证明

为了证明AddElement，我们需要证明b == Sum(t)在它的最终状态是成立的。回顾作业，这意味着我们需要展示

a + y == Sum(s + {y})

在初始状态。由于a是Sum(s)，我们的证明义务可以归结为

Sum(s) + y == Sum(s + {y})

我们已知y不在s中。

假设Pick(s + {y})返回y。然后,我们有

  Sum(s + {y});
==  // def. Sum
  var x := Pick(s + {y}); x + Sum(s + {y} - {x});
==  // using the assumption Pick(s + {y}) == y
  y + Sum(s + {y} - {y});
==  // sets, since y !in s
  y + Sum(s);

这很简单也很直接。但对于这个证明，我们假设对Pick的相关调用返回了y。如果Pick返回与s不同的元素怎么办?

选择其他东西

在你意识到“挑选”可以选择一个不同于你所想的元素之前，乌云开始散去。我们需要的是一个引理，它表明选择是无关紧要的。也就是说，引理会让我们把“Sum”看作是，在做递归调用时，我们指定的一个元素。

这就是那个引理。这个证明一开始也有点棘手。归根到底就是让“Pick”选择它所选择的任何元素，然后对“Sum”递归的更小的集合应用归纳假设。

lemma SumMyWay(s: set<int>, y: int)
  requires y in s
  ensures Sum(s) == y + Sum(s - {y})
{
  var x := Pick(s);
  if y == x {
  } else {
    calc {
      Sum(s);
    ==  // def. Sum
      x + Sum(s - {x});
    ==  { SumMyWay(s - {x}, y); }
      x + y + Sum(s - {x} - {y});
    ==  { assert s - {x} - {y} == s - {y} - {x}; }
      y + x + Sum(s - {y} - {x});
    ==  { SumMyWay(s - {y}, x); }
      y + Sum(s - {y});
    }
  }
}

我说这个引理看起来像Sum的表达式，所以Sum的两个参数是s和s - {y}。或者，我们可以用s + {y}和s来调用Sum来声明该属性。这个选择是上述引理的一个简单推论:

lemma AddToSum(s: set<int>, y: int)
  requires y !in s
  ensures Sum(s + {y}) == Sum(s) + y
{
  SumMyWay(s + {y}, y);
}

使用引理

有了这个有用的引理，就很容易得到“AddElement”的证明:将其主体更改为

t := s + {y};
b := a + y;
AddToSum(s, y);

内联选择

在上面的开发中，我将‘Pick’定义为一个单独的函数。阅读程序文本中的单词“pick”可能有助于理解“Sum”和“SumMyWay”做什么。但它是一个如此小的函数，所以为什么不直接在使用它的两个地方内联它呢。让我们试一试:

function Sum(s: set<int>): int {
  if s == {} then 0 else
    var x :| x in s;  // this line takes the place of a call to Pick
    x + Sum(s - {x})
}

lemma SumMyWay(s: set<int>, y: int)
  requires y in s
  ensures Sum(s) == y + Sum(s - {y})
{
  var x :| x in s;  // this line takes the place of a call to Pick
  if y == x {  // error: postcondition might not hold on this path
  } else {
    calc {
      Sum(s);
    ==  // def. Sum        // error: this step might not hold
      x + Sum(s - {x});
    ==  { SumMyWay(s - {x}, y); }
      x + y + Sum(s - {x} - {y});
    ==  { assert s - {x} - {y} == s - {y} - {x}; }
      y + x + Sum(s - {y} - {x});
    ==  { SumMyWay(s - {y}, x); }
      y + Sum(s - {y});
    }
  }
}

现在我们得到两个错误!

为了解释发生了什么，让我多说一点关于:|以及它的不同寻常之处。

Let such that

Dafny中的let-such-that结构有这样一种形式

var x :| P; E

它的计算结果是E，其中x被绑定到某个满足P的值。例如,

var x :| 7 <= x < 10; 2 * x

计算结果为“14”、“16”或“18”。作为程序员，你无法控制选择x的哪个值。但你会知道两件重要的事。一是x将被选为满足P的值。(如果Dafny验证器不能证明这样的值存在，则会给出一个错误。)另一种方法是，每次使用相同的输入对表达式求值时，都将得到相同的值。换句话说，这个算子是确定性的。

下面是另一个关于决定论的例子:

var x :| x in {2, 3, 5}; x

这个表达式选择x为最小的三个素数之一(2、3或5)，然后返回它。您不知道您得到的是这三个值中的哪一个，但您可以保证每次在程序的一次运行中计算这个表达式时，您将得到相同的值。

让我们更准确地理解我所说的“这个表达”。在Dafny中，let-such-that表达式的每一个“文本出现”都可以做出自己的选择。考虑这个问题的一种方法是遍历程序的文本，并用唯一的颜色为每个:|操作符着色。然后，你可以依赖于相同的选项，只有当它们由相同颜色的:|执行时。

这里有一个说明性的例子。

lemma Choices(s: set<int>)
  requires s != {}
{
  var a := Pick(s);
  var b := Pick(s);
  assert a == b;  // this is provable
  a := var x :| x in s; x;
  b := var x :| x in s; x;
  assert a == b;  // error: not provable
}

赋给a和b的第一个值来自相同的:|操作符。它们是相同颜色选择的结果。因此，它们被认为是相同的。相反，赋给a和b的下一个值来自不同的:|操作符——不同颜色的操作符。因此，您不能确定‘a’和‘b’是相等的。

实际上，如果你多想一点(或者少想一点)，你就会意识到，我们知道赋给a和b的第一个值是相等的，即使不知道Pick的任何内容。毕竟，Pick是一个函数，如果你对相同的参数调用一个函数两次，它会返回相同的值。数学保证了这一点，Dafny也是如此。那么，对a和b的第二个赋值呢;那些表达式中的:|操作符不也是函数吗?是的，它们是，但它们是不同的功能。它们是不同颜色的函数，以此类推。只要你把程序中出现的每一个:|看作是一个不同的函数，那么所有的数学运算就会如你所期望的那样。

这就是为什么我可以更容易地描述“Sum”的情况，如果我可以使用一个“😐”。为了重用相同的:|，我把它放在一个函数中，我命名为Pick。我建议你做同样的事情如果你在处理涉及到你想要证明属性的选择的幽灵函数。

多种选择

在理解这些问题之前，如果你试图定义“Sum”并在“AddElement”中使用它，你会感到困惑。现在，您知道单独将:|放入函数中更容易，并且您知道您需要编写一个类似SumMyWay的引理。您可能会好奇，如果没有Pick函数，是否可以做到这一点。也就是说，你可能想知道是否有任何方法可以在Sum中使用一个:|操作符，在SumMyWay中使用另一个:|操作符。是的，这是可能的。我来教你怎么做。

假设我们在函数Sum中内联Pick。也就是说，假设我们像上面4 (opens new window)节那样定义“Sum”。在那一节中，我提到，如果你也内联Pick在SumMyWay，你会得到一些错误。这两个错误都是因为“Sum”和“SumMyWay”做出了不同的选择。但我们可以在引理中更具体一些，强制它选择与Sum中选择的元素相同的元素。

你可以这样做，你想让x不只是在s中，而是一个值

Sum(s) == x + Sum(s - {x})

没错。只有一个这样的x存在，它是由“Sum”选择的。所以，如果你这样写引理:

lemma SumMyWay(s: set<int>, y: int)
  requires y in s
  ensures Sum(s) == y + Sum(s - {y})
{
  var x :| x in s && Sum(s) == x + Sum(s - {x});
  if y == x {
  } else {
    // same calc statement as before...
  }
}

然后验证!知道这一点很好，但是在你的:|周围引入Pick函数似乎更干净。

总结

注意，程序中出现的每一个:|文本都是一个不同的函数。如果你将它整合到一个你命名的函数中，你将更容易使用:|，因为这样你就减少了因为不同种类(不同“颜色”)的选择而感到困惑的机会。

另外，请注意:|所做的选择可能不是您需要的选择。你可能想要证明一个引理，它说任何选择最后都会得到相同的结果。使用上面的“SumMyWay”引理作为你的证明模板。