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;
}
这是定义排序集、排序映射、范围集的一小步。