如何在 Dafny 中对序列中的整数进行排序？

Question

正如标题所说，我想对序列进行排序（而不是数组，这更容易）。但我遇到了很多问题（例如，不同数据类型之间的转换，因为序列是不可变的）。甚至冒泡排序也无法为我证明。有什么想法吗？

具体来说，目标如下

method sort(a: seq<int>) returns (r: seq<int>)
  ensures |a| == |r|
  ensures multiset(a) == multiset(r)
  ensures forall i,j :: 0 <= i <= j < |r| ==> r[i] <= r[j]
{
  // implemetion here
}

Answer 1

学习 Dafny 需要一段时间。您将需要学习该语言的语法和语义。 Dafny 中的验证算法几乎总是归结为某些属性或其他属性的归纳，因此开始思考和练习归纳证明。

我推荐 Rustan Leino 的《Program Proofs》一书和他的 Dafny 高级用户网站。那里有一些关于 Dafny 的小博客文章。我写了一个半教程半问题解释的小系列博客这里.

我已经在这里和程序校样文件夹第15章中验证了一些排序示例。