Dafny "컨텍스트의 수정 조항을 위반할 수 있습니다"

Question

해시 세트를 확인하려고하는데 삽입 방법에 문제가 있습니다.

main에서 삽입 주석을 제거 할 때 "호출이 컨텍스트의 수정 절을 위반할 수 있습니다."라는 오류가 나타나는 이유를 모르겠습니다. 나는 그것을 신선한 것의 사용과 관련이 있다고 믿지만, 어떻게/어디에서해야할지 명확하지 않다.

코드에서 찾을 수 있습니다 : https://rise4fun.com/Dafny/9UDG

Answer 1

문제는 삽입 후 insert의 최초의 호출은 임의의 무언가를 가리 키도록 a 필드를 변경 가능성을 열어 둡니다하는 this 및 a을 수정하고 주장 즉 insert에 대한 두 번째 호출은 임의의 것을 수정합니다.

간단한 해결책은 ensures a == old(a)을 insert에 추가하는 것입니다.