변경된 개체에 대한 절 오류 수정

Question

" "이 메서드에서 반환 한 개체가 "new"가되도록 보장 할 수있는 방법 (Dafny에서)은 어디에서나 사용되는 개체와 동일하지 않습니다. 그렇지 않으면 (아직)?

다음 코드는 최소한의 예를 보여줍니다

method newArray(a:array<int>) returns (b:array<int>) 
requires a != null 
ensures b != null 
ensures a != b 
ensures b.Length == a.Length+1 
{ 
    b := new int[a.Length+1]; 
} 

class Testing { 
    var test : array<int>; 

    method doesnotwork() 
    requires this.test!=null 
    requires this.test.Length > 10; 
    modifies this 
    { 
    this.test := newArray(this.test); //change array a with b 
    this.test[3] := 9; //error modifies clause 
    } 

    method doeswork() 
    requires this.test!=null 
    requires this.test.Length > 10; 
    modifies this 
    { 
    this.test := new int[this.test.Length+1]; 
    this.test[3] := 9; 
    } 


} 

은 "doeswork"기능 컴파일 (및 검증한다) 제대로을하지만, Dafny 컴파일러는 객체가 반환 된 것을 알 수 없기 때문에, 다른 하나는하지 않습니다 "newArray"함수는 새로운 함수입니다. 즉, "doesnotwork"함수의 "require"문에서 수정할 수있는 것으로 표시 할 필요가 없습니다.이 함수는 "this "입니다. "doeswork"함수에서 "newArray"함수의 정의를 삽입하기 만하면됩니다.

위의 예는 https://rise4fun.com/Dafny/hHWwr에 있으며 온라인에서도 실행될 수 있습니다.

감사합니다.

Answer 1

ensures fresh(b)은 newArray에 올 수 있습니다.

fresh은 사용자가 설명한 것과 같습니다. 개체는 newArray 호출 전에 할당 된 개체와 다릅니다.