Dafny泛型類型數組錯誤

在試圖驗證數組支持的通用FIFO隊列時，我遇到了一個令人困惑的錯誤。該隊列被發現在this論文中，由Dafny的創建者撰寫。Dafny泛型類型數組錯誤

在考慮中的錯誤是：

除非一個初始化設置爲陣列的元素，「數據」的一個新的數組必須具有涉及兩行分配一個空的大小

數組通過new Data[whatever]在構造函數和enqueue方法中。

Dafny版本：Dafny 2.0.0.00922技術預覽參考0

的完整代碼。

class {:autocontracts} SimpleQueue<Data> 
{ 
    ghost var Contents: seq<Data>; 
    var a: array<Data>; 
    var m: int, n: int; 
    predicate Valid() { 
     a != null && a.Length != 0 && 0 <= m <= n <= a.Length && Contents == a[m..n] 
    } 
    constructor() 
    ensures Contents == []; 
    { 
     a := new Data[10]; 
     m := 0; 
     n := 0; 
     Contents := []; 
    } 
    method Enqueue(d: Data) 
    ensures Contents == old(Contents) + [d]; 
    { 
     if n == a.Length { 
      var b := a; 
      if m == 0 { 
       b := new Data[2 * a.Length]; 
      } 
      forall (i | 0 <= i < n - m) { 
       b[i] := a[m + i]; 
      } 
      a, m, n := b, 0, n - m; 
     } 
     a[n], n, Contents := d, n + 1, Contents + [d]; 
    } 

    method Dequeue() returns (d: Data) 
    requires Contents != []; 
    ensures d == old(Contents)[0] && Contents == old(Contents)[1..]; 
    { 
     assert a[m] == a[m..n][0]; 
     d, m, Contents := a[m], m + 1, Contents[1..]; 
    } 
} 
method Main() 
{ 
    var q := new SimpleQueue(); 
    q.Enqueue(5); q.Enqueue(12); 
    var x := q.Dequeue(); 
    assert x == 5; 
}

來源

2017-10-18 DaKellyFella