Dafny Вставить int в метод Sorted Array

Question

Я пытаюсь доказать эту программу в dafny, но я все еще получаю сообщение об ошибке с последним инвариантом, и я не понимаю, почему он не работает.

Программа состоит из метода, который вставляет int в отсортированный массив. Интер будет вставлен в правильное положение, т.е.: вставка 5 в 1,2,3,4,5,6,7 будет возвращаться: 1,2,3,4,5,5,6,7

function sorted (a: array<int>): bool 
    requires a != null ; 
    reads a; 
    { 
    forall i :: 0 <= i < (a.Length - 1) ==> a[i] <= a[ i+1] 
    } 

method InsertSorted(a: array<int>, key: int) returns (b: array<int>) 
    requires a != null && sorted(a); 
    ensures b != null ; 
    ensures sorted(b); 
    { 
    var i:= 0; 
    b:= new int[a.Length + 1]; 

    if(a.Length > 0){ 
     while (i < a.Length) 
     invariant 0<= i; 
     invariant i <= a.Length; 
     invariant b.Length == a.Length + 1; 
     invariant sorted(a); 
     invariant forall j :: 0 <= j < i ==> b[j] <= b[j+1]; 
     { 
     if(a[i]<=key) 
     { 
      b[i]:= a[i]; 
      b [i+1] := key; 
      assert b[i] <= b[i+1];   
     } 
     else if (key > a[i]) 
     { 
      if(i==0) 
      { 
      b[i] := key; 
      } 
      b [i+1] := a[i]; 
      assert key > a[i]; 
      assert b[i]<= b[i+1]; 
     } 
     else{ 
      b[i]:= a[i]; 
      b [i+1] := a[i]; 
      assert sorted(a); 
      assert b[i] <= b[i+1]; 
     } 
     assert b[i]<= b[i+1]; 
     i := i+1; 
     } 
    } 
    else{ 
     b[0] := key; 
    } 
    } 

Спасибо

Answer 1

Я думаю, что, возможно, у вас алгоритм неправильный. В любом случае, я считаю, что усложнения трудно понять, если первая ветвь не занята, то мы знаем, что !(a[i] <= key) или просто a[i] > key, что подразумевает, что вторая ветвь, защищенная key > a[i], недоступна.

!(a[i]<=key) && a[i] < key ==> false 

В любом случае, я подозреваю, что инвариант цикла не является достаточно сильным, чтобы доказать даже правильный вариант, так как вы не отслеживания состояния b достаточно подробно.

Ниже приведено доказательство алгоритма, аналогичного вашему, показывающего более сильный инвариант цикла. Я отслеживаю, где в массиве key вставляется с помощью призрачной переменной (переменная, которая используется только для проверки и не будет отображаться в выводе компилятора).

http://rise4fun.com/Dafny/RqGi

predicate sorted (a: seq<int>) 
{ 
forall i,j :: 0 <= i < j < |a| ==> a[i] <= a[j] 
} 

predicate lessThan(a:seq<int>, key:int) { 
forall i :: 0 <= i < |a| ==> a[i] < key 
} 

predicate greaterEqualThan(a:seq<int>, key:int) { 
forall i :: 0 <= i < |a| ==> a[i] >= key 
} 

method InsertSorted(a: array<int>, key: int) returns (b: array<int>) 
    requires a != null && sorted(a[..]) 
    ensures b != null && sorted(b[..]); 
{ 
b:= new int[a.Length + 1]; 

ghost var k := 0; 
b[0] := key; 

ghost var a' := a[..]; 

var i:= 0; 
while (i < a.Length) 
    modifies b; 
    invariant 0 <= k <= i <= a.Length 
    invariant b.Length == a.Length + 1 
    invariant a[..] == a' 
    invariant lessThan(a[..i], key) ==> i == k; 
    invariant lessThan(a[..k], key) 
    invariant b[..k] == a[..k] 
    invariant b[k] == key 
    invariant k < i ==> b[k+1..i+1] == a[k..i] 
    invariant k < i ==> greaterEqualThan(b[k+1..i+1], key) 
    invariant 0 <= k < b.Length && b[k] == key 
    { 
    if(a[i]<key) 
    { 
     b[i]:= a[i]; 
     b[i+1] := key; 
     k := i+1; 
    } 
    else if (a[i] >= key) 
    { 
     b[i+1] := a[i]; 
    } 
    i := i+1; 
    } 
    assert b[..] == a[..k] + [key] + a[k..]; 

}