Dafny 컨텍스트 수정 절 오류

Question

내 Dafny 프로그램에서 마지막 오류를 제거하는 데 어려움을 겪고 있습니다. 누군가 올바른 방향으로 나를 가리킬 수 있습니까? 나는이 오류를 얻고있다 http://rise4fun.com/Dafny/2FPo

: 여기 는 코드 할당하지 바깥 쪽 문맥의 수정 절에 배열 요소를 업데이트 할 수 있습니다

내가 추가 수정 내가 확신에도 불구하고 병합 방법 (에 직사각형 시도

) 이미 병합 메서드 호출에 비슷한 오류가 발생합니다.

나는 이걸 정말로 잃어 버렸습니다. 도움을 주셔서 감사합니다

Answer 1

문제는 "수정"이 해당 필드에 의해 수정 된 것들이 아니라 필드의 수정을 허용합니다. 방법 일 경우 즉,이 적절할 것 :

this.rectangles := new_rectangle_array; 

하지만이 일을 한 경우 :

가

this.rectangles[3] := new_rect; 

그래서, 당신이 가지고있는 장소에서 "이 수정"대신해야 "직사각형을 수정합니다".

비슷한 이유로 Test에 "c"를 수정하지 않고 "modify c.rectangles"를 주석으로 추가해야합니다.

마지막으로 Dafny가 Test를 호출 할 수 있다고 확신 시키려면 Couverture의 생성자에게 직사각형 필드를 제약 한 사후 조건을 제공해야합니다. 그렇지 않으면 검증자는 Test를 호출해도 괜찮은지 확신 할 수 없습니다. 검증자가 알 수있는 한 couv는 Main이 수정할 수없는 임의의 배열을 포함 할 수 있습니다.

전체 코드는 http://rise4fun.com/Dafny/Skrg을 참조하십시오.