问题[dafny](coding)

这是一个类似的问题，但我还没能把它映射到我的用例中。基本上，我想用 Dafny 证明一个带有嵌套量词的基本命题（对于所有 X，都存在 Y），该命题在整数上的一阶逻辑中。我选择的具体命题是：该abs函数在非负整数上是全射。以下是一段精简的代码片段：

function abs(x: int): int {
    if x > 0 then x else -x
}

// Passes the verifier
lemma AbsSurjectiveFor(y: int)
requires y >= 0
ensures exists x :: abs(x) == y
{
    assert abs(y) == y;
}

// Error in this lemma (universal generalization of the above)
lemma AbsSurjective()
ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
{
    // Forall introduction syntax
    forall y: int | y >= 0
    ensures exists x :: abs(x) == y
    {
        AbsSurjectiveFor(y);
    }
}

问题

上述使第二个引理通过的正确语法是什么？

更概括地说，如果我想手动进行证明（比如，以自然演绎的方式），我正在寻找 forall-introduction 和 forall-elimination 规则的语法。我怀疑自己做了一些非常“明显”的错误，但在参考手册中找不到正确的语法。

笔记

Dafny 证明了第一个引理（很简单，不需要引入量词），但是第二个引理却失败了，尽管我完全匹配了Rustan 的答案中给出的语法，该答案建议在引理中使用 forall 语句块。

关于可能出错的地方，我收到了关于使用不带触发器的量词的警告。但是，我并不特别在意触发器，因为我的目的是手动证明 forall/exists 语句。我不确定是否有办法直接关闭触发器，或者告诉 Dafny 根本不要实例化量词，除非我指示它这样做。

输出dafny verify：

$ dafny verify fol-minimal.dfy 
fol-minimal.dfy(15,8): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(18,4): Warning: Could not find a trigger for this quantifier. Without a trigger, the quantifier may cause brittle verification. To silence this warning, add an explicit trigger using the {:trigger} attribute. For more information, see the section quantifier instantiation rules in the reference manual.
   |
18 |     forall y: int | y >= 0
   |     ^^^^^^^^^^^^^^^^^^^^^^

fol-minimal.dfy(16,0): Error: a postcondition could not be proved on this return path
   |
16 | {
   | ^

fol-minimal.dfy(15,8): Related location: this is the postcondition that could not be proved
   |
15 | ensures forall y: int :: y >= 0 ==> exists x :: abs(x) == y
   |         ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Dafny 有以下几种方式来声明支持相等的类型。

T(==)

但是有没有办法指定类型支持排序（<, <=, >, >=）等？

我正在尝试用 Dafny 编写一个“线性搜索”方法。该方法采用将f自然数映射到布尔值的函数，并且已知存在第一个数字，n使得f(n) == True。然后该方法确保 n是返回值。根据此规范，
自然n可以是任意大的，并且只有在假设可用能量任意大的情况下，才能确保程序能够找到n。

这难道不是达芙妮无法表达的吗？

这是我尝试过的

method linear_search(f: nat -> bool) returns (x: nat)
    requires exists n : nat :: f(n)
    ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
    x := 0;
    while !f(x)
    {
        x := x + 1;
    }
}

验证器失败：“无法证明终止；尝试为循环提供减少子句”

另一种有界线性搜索已得到验证，没有任何问题。

method bounded_linear_search(f: nat -> bool, max_bound: nat) returns (x: nat)
    requires exists n : nat :: n <= max_bound && f(n)
    ensures f(x) && forall i : nat :: i < x ==> !f(i)
{
    x := 0;
    while !f(x) && x <= max_bound
        decreases max_bound - x
        invariant forall i : nat :: i < x ==> !f(i)
    {
        x := x + 1;
    }
}

我们如何证明如果对于所有输入，f并且g返回相同的输出，那么这两个函数是等价的？

lemma func_ext(f: int -> int, g: int -> int)
requires forall x :: f(x) == g(x)
ensures f == g

我认为这是一个公理，但它不起作用。Dafny 中的函数外延性不成立吗？

lemma blah(p:nat->bool, xs:seq<nat>)
  requires forall t | t in xs :: p(t)
  ensures forall i | 0 <= i < |xs| :: p(xs[i]) {}

lemma zero_is_zero(xs:seq<nat>)
  requires forall x | x in xs :: (x == 0)
  ensures forall k | 0 <= k < |xs| :: (xs[k] == 0) {
  // blah(x => x == 0, xs);
}

所以，我正在尝试 dafny 版本4.4.0，并且正在努力理解上面的代码片段。它大致匹配这里两个相关引理之一；但我稍微简化了它们。

我的理解是，zero_is_zero引理基本上是引理的概括（本例中的blah属性是）。因此，如果有的话，自动验证应该更容易。我期望通过索引访问时，序列中的元素将被视为与同一元素无法区分。px => x == 0zero_is_zero

在实践中，事实证明这blah是自动验证的（即我在引理主体中没有做任何事情）。但因为zero_is_zero我必须显式调用blah以表明它确实适用于 property x => x == 0，然后突然间它不再是问题了。

对此有何解释？

谢谢！

我在 Dafny 有一个 nat 数组，我想以非线性方式遍历它。为了阐明问题：考虑一个数组，这样（请暂时忽略语法）：

var links : array<nat>;

links := [1,2,5,4,0,3];

在给定索引“i”处，links[i]保存必须考虑的下一个元素的索引。在这里，让i == 2 ==> links[i] == 5. 在下一次迭代中，循环读取索引 5 处的值，即 3，依此类推，直到links[i] == 0。

我已经实现了 while 循环和一些似乎无法证明终止的谓词。

第一个谓词是列表中的每个元素都是唯一的，并且没有元素大于循环的长度。之所以如此，是因为否则数组就会变成圆形。谓词来自这里。

forall i, j | 0 <= i < links.Length && 0 <= j < links.Length && i != j :: links[i] != links[j]

第二个谓词是数组中存在一个元素为 0。这是终止条件。

exists q :: 0 <= q < links.Length && links[q] == 0

while 循环迭代如下：

qAct = links[0];

while(qAct != 0)
/* invariants and decreases ??? */
{
qAct = links[qAct];
}

这里的问题是 qAct 并没有真正减少。为了解决这个问题，我推断循环的迭代永远不会超过其长度，所以我尝试：

qAct = links[0];
var i : nat;
i := 0

while(qAct != 0 && i < links.Length)
/* this terminates */
decreases links.Length - i
{
qAct := links[qAct];
i := i + 1;
}

原因是，根据数组的设计，元素的数量不能大于数组的长度。因此，循环最多迭代 links.Length 次。

有没有办法在不使用“i”的情况下证明终止？我还尝试将“i”定义为幽灵变量，但收到一条错误消息“在此上下文中不允许分配给非幽灵变量”。在qAct := links[qAct]。

带有霍尔逻辑（和简单推理）的笔和纸证明足以表明 qAct 由于第二个谓词最终收敛到 0。但达夫尼未能用这个谓词进行推理。

有达夫尼经验的人的帮助是无价的！

我正在尝试在 Dafny 中调试变量验证时间。我尝试运行verificationLogger，但没有得到任何输出。

• 我使用的是 Windows（但对 Linux 解决方案很满意）

• 我将路径设置为 VSCode 加载项安装的 Dafny 版本，如下所示：

  设置路径=C:\Users\carlk.vscode-insiders\extensions\dafny-lang.ide-vscode-3.1.2\out\resources\4.2.0\github\dafny;%path%

• 我跑：

  dafny verify --verification-time-limit:15 --cores:6 --boogie -randomSeedIterations:10 --boogie -verificationLogger:csv repro1.dfy

但我没有看到 CSV 输出。

我在 Dafny 中创建了一个经过验证的 SortedMap。它是（键，值）对的序列。键是排序的、不同的整数。我不知道如何表明“KeySet”的长度必须等于序列的长度。

——卡尔

错误：

this is the postcondition that could not be proved
  |
7 |   ensures |KeySet(sorted_seq)| == |sorted_seq|

简化代码：

predicate SortedSeq(sequence: seq<(int, int)>) {
  forall i, j | 0 <= i < j < |sequence| :: sequence[i].0 < sequence[j].0
}

function KeySet(sorted_seq: seq<(int, int)>): set<int>
  requires SortedSeq(sorted_seq)
  ensures |KeySet(sorted_seq)| == |sorted_seq|
{
  set i | i in sorted_seq :: i.0
}


method Main()
{
  var s: seq<(int,int)> := [(1, 2), (30, 40), (50, 50)];
  print KeySet(s);

}

我对任何可验证的 CountLessThan 编写方式持开放态度。这是我所拥有的：

function SetLessThan(numbers: set<int>, threshold: int): set<int>
{
  set i | i in numbers && i < threshold
}
method CountLessThan(numbers: set<int>, threshold: int) returns (count: int)
  ensures count == |SetLessThan(numbers, threshold)|
{
  count := 0;
  var shrink := numbers;
  var grow := {};
  while |shrink | > 0
    decreases shrink
    invariant shrink + grow == numbers
    invariant count == |SetLessThan(grow, threshold)|
  {
    var i: int :| i in shrink;
    shrink := shrink - {i};
    grow := grow + {i};
    if i < threshold {
      count := count + 1;
    }
  }
}

method Main()
{
  var s: set<int> := {1, 2, 3, 4, 5};
  var c: int := CountLessThan(s, 4);
  print c;
  // assert c == 3;

}

这是定义排序集、排序映射、范围集的一小步。