specifications - Dafny 无法证明整数数组中的最大元素

Question

我试图在 Dafny 中证明一个简单的程序，它可以找到整数数组的最大元素。Dafny在几秒钟内成功地证明了下面的程序。当我从最后两个规范中删除注释ensures时，Dafny 会发出错误消息说

a postcondition might not hold on this return path

这可能是由index保证为<= a.Length. 但是，max_index < a.Length是正确的，我很难证明这一点。我尝试在语句中编写嵌套不变量if，但 Dafny 拒绝了该语法。任何可能的解决方案？这是我的代码：

method FindMax(a: array<int>) returns (max: int, max_index : int)
    requires a.Length > 0
    ensures forall k :: 0 <= k < a.Length ==> a[k] <= max
    ensures 0 <= max_index
    // ensures max_index < a.Length
    // ensures a[max_index] == max
{
    max := 0;
    var index := 0;
    max_index := 0;
    while index < a.Length
        invariant 0 <= index <= a.Length
        invariant forall k :: 0 <= k < index ==> a[k] <= max
    {
        if (max  < a[index])
            // invariant 0 <= index < a.Length
        {
            max := a[index];
            max_index := index;
        }
        index := index + 1;
     }
}

Answer 1

事实证明，我的循环不变量需要更仔细的计划。这是正确的版本：

method FindMax(a: array<int>) returns (max: int, max_index : int)
    requires a.Length > 0
    ensures forall k :: 0 <= k < a.Length ==> a[k] <= max
    ensures 0 <= max_index
    ensures max_index < a.Length
    ensures a[max_index] == max
{
    var index := 0;
    max_index := 0;
    max := a[max_index];
    while index < a.Length
        invariant max_index < a.Length
        invariant 0 <= index <= a.Length
        invariant forall k :: 0 <= k < index ==> a[k] <= max
        invariant a[max_index] == max
    {
        if (max  < a[index])
        {
            max := a[index];
            max_index := index;
        }
        index := index + 1;
     }
}

Dafny 需要 10 多秒的时间来证明。