Dafny 제네릭 형식 배열 오류

Question

배열로 백업 된 일반 FIFO 큐를 확인하는 중 혼란스러운 오류가 발생했습니다. 대기열은 Dafny의 작성자가 작성한 this 종이에서 발견되었습니다.

해당 오류 : 이니셜 라이저가 배열 요소를 구비

않으면, '데이터'의 새로운 어레이가 할당 양쪽 라인에 관한 빈 크기

있어야 배열을 new Data[whatever]을 통해 생성자와 큐 삽입 메서드에 추가합니다.

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

Answer 1

Dafny의 형식 시스템은 "기본적으로 초기화 할 수없는"형식을 지원하기 위해 일반화되었습니다. 이로 인해 일부 비 호환성이 발생했습니다.

가장 쉬운 수정 변경하는 것입니다

class SimpleQueue<Data> 

유형이 변수 Data 만 기본적으로 initializable 유형 인스턴스화 할 수 있음을 의미

class SimpleQueue<Data(0)> 

합니다.

또 다른 해결 방법은 Data 유형의 기본값을 인수로 사용하도록 생성자를 변경하는 것입니다. 그런 다음 이니셜 라이저 함수를 사용하여 배열을 할당 할 수 있습니다 (예 :

new Data[10] (_ => d) 

).