dafny의 배열 덮어 쓰기

Question

메소드 내부의 배열을 덮어 쓰려고합니다. 컴파일러에서 나에게 오류 "오류 : 할당의 LHS가 가변 변수를 나타내야합니다"를 표시합니다.

나는 눈이 멀어서 뭔가를 놓치고 있거나 왜 Dafny가 이것을 허용하지 않습니까?

Answer 1

Dafny에서 메서드 매개 변수를 할당 할 수 없습니다. 내부적으로 값을 업데이트해야하는 경우 로컬 변수를 사용할 수 있습니다. 이 새로운 배열이 호출자에게 사용 가능하게하려면 예를 들어

,

var a' := new int[0]; 

은 또한 그것을 반환해야합니다.

return a';  

즉, 전체 정렬 방법을 쓰고 싶다면이 작업을 수행 할 필요가 없습니다. 그냥 a을 수정하십시오.

a[0] := 0; 
// ...