問題タブ [dafny]
For questions regarding programming in ECMAScript (JavaScript/JS) and its various dialects/implementations (excluding ActionScript). Note JavaScript is NOT the same as Java! Please include all relevant tags on your question; e.g., [node.js], [jquery], [json], [reactjs], [angular], [ember.js], [vue.js], [typescript], [svelte], etc.
verification - Dafny 事後条件メッセージに混乱
非常に単純な乗算コード:
ダフニーで確認すると、次のように表示されます。
いくつかの条件下で res != m*n と表示されますが、わかりません。
verification - Dafny 事後条件メッセージに混乱
非常に単純な乗算コード:
ダフニーで確認すると、次のように表示されます。
いくつかの条件下で res != m*n と表示されますが、わかりません。
verification - ダフニーは失敗したアサーションの反例を示すことができますか?
Dafnyを使って以下のプログラムの正誤を証明しようとしています。
Dafny は、アサーションが正しくないことを証明することに成功しました。ただし、アサーションが失敗した例は示していません。Dafny だけでそのような例を挙げることができますか?
z3 - 正しい Dafny メソッドの Z3 モデル
正しいメソッドの場合、Z3 はメソッドの検証条件のモデルを見つけることができますか?
私はそうではないと思っていましたが、これはメソッドが正しい例です
それでも、検証によってモデルが見つかります。
これは Dafny 1.9.7 で発生しました。
formal-verification - Dafny は N 以下の偶数を収集します
limこれは、整数を取り、それより厳密に小さいlim偶数のすべての整数のシーケンスを返す例です。
2 番目の不変量の逆方向のみが... <==> ...検証されません。私はしばらくこれをいじってみましたが、理解できませんでした。
どんな助けでも大歓迎です！