specifications - Dafny 未能证明整数数组中的最大元素

Question

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

a postcondition might not hold on this return path

这可能是由于 index保证为 <= a.Length 。然而，max_index < a.Length是正确的，但我很难证明它。我尝试在 if 中编写嵌套不变量声明，但达夫尼拒绝了这种语法。有什么可能的解决办法吗？ 这是我的代码:

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;
     }
}

达夫尼花了 10 秒多一点的时间来证明。