Dafny「呼び出しがコンテキストの変更句に違反する可能性があります」

Question

ハッシュセットを検証しようとしていますが、挿入メソッドに問題があります。

mainの挿入をアンコメントすると、なぜ「コンテキストの変更句に違反する可能性があります」というエラーが出るのか分かりません。私はそれが新鮮なものの使用と関係があると信じていますが、どうやってこれをやるべきかは不明です。

コードで見つけることができます。問題は、インサートが、その後insertへの最初の呼び出しは、任意のものを指すようにaフィールドを変更している可能性を開いたままにされ、thisとaを変更すると主張し、ということであるhttps://rise4fun.com/Dafny/9UDG

Answer 1

insertへの2番目の呼び出しは、その任意のものを変更します。

ensures a == old(a)をinsertに追加するのが簡単な解決方法です。