主页 / coding / 问题 / 79171789
Accepted
Germán Ferrero
Asked: 2024-11-09 06:58:40 +0800 CST

我们可以为 Dafny 中的循环变量设置任意大的上限吗？

  • 772

我正在尝试用 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;
    }
}
dafny

1 个回答

  1. Best Answer

    您可以使用幽灵变量以及向循环添加必要的不变量来验证原始版本。幽灵变量是一种变量，可用于保留其他信息以供验证，但不是可编译代码的一部分。

    module SO6 {
    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)
    {
        ghost var n: nat :| f(n);
        x := 0;
        while !f(x)
            invariant x <= n
            invariant forall i : nat :: i < x ==> !f(i)
            decreases n - x
        {
            x := x + 1;
        }
        assert f(x);
    }

}
    • 0

相关问题