Dafny 无法证明整数数组中的最大元素答案

【问题标题】：Dafny fails to prove max element in integer arrayDafny 无法证明整数数组中的最大元素
【发布时间】：2019-10-18 04:14:09
【问题描述】：

我试图在 Dafny 中证明一个简单的程序，它可以找到整数数组的最大元素。 Dafny 成功在几秒钟内证明了下面的程序。当我从最后两个 ensures 规范中删除 cmets 时，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;
     }
}

【问题讨论】：

标签： specifications dafny loop-invariant

【解决方案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 多秒的时间来证明。

【讨论】：