Дафни не может доказать максимальный элемент в целочисленном массиве - PullRequest
Новая
       49

Дафни не может доказать максимальный элемент в целочисленном массиве

1 голос
/ 02 июня 2019

Я пытаюсь доказать простую программу на Дафни, которая находит максимальный элемент целочисленного массива. Дафни преуспевает через несколько секунд, доказывая программу ниже. Когда я удаляю комментарии из последних двух ensures спецификаций, Дафни запускает сообщения об ошибках, в которых говорится, что 

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

1 Ответ

1 голос
/ 02 июня 2019

Оказывается, мои инварианты цикла нуждались в более тщательном планировании.Вот правильная версия: 

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 секунд, чтобы доказать.

...