問題タブ [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.
dafny - 1 つの Dafny ファイルを別の Dafny ファイルに含める
複数のプログラムで同じ Dafny コードを再利用したい。ある Dafny ファイルを別の Dafny ファイルに含めることはできますか? マニュアルには、それを行う方法については説明されていません。
verification - メソッドの実行前と実行後の状態の間の関係を定式化する方法は?
私は次のzaMapを持っています(ここで完全なコードを参照してください: http://rise4fun.com/Dafny/LCaM ):
putここで、メソッドにさらに仕様を追加したいと思います。たとえばensure、戻り値が の場合、関数呼び出しの前にsuccess == trueマップがあったこと、または同等にマップが でない場合、そこに保証されることを望みます。!full()full()put
問題は、前提条件「必須」では何が返されるかまだわからず、事後条件「保証」では元のマップがもうないことです。人々はそれについて何をしますか？
arrays - 配列を含むこの Dafny アサーションが失敗するのはなぜですか?
私はガウス消去法の検証済み実装に取り組んでおり、配列 b の内容を配列 a の内容に追加するこの非常に単純な方法の検証に問題があります。これがコードです。
if-statement - Dafny - if ステートメント内でメソッドを呼び出しますか?
タイトルが示すように、次のような別のメソッドの if ステートメント内のいくつかの変数を変更するメソッドを呼び出したいと思います。
Dafny は非ゴースト メソッドをそのような方法で呼び出すことを許可しないため、これは機能しません。この問題の回避策は何ですか?
arrays - Dafny: コピー アレイ リージョン メソッドの検証
検証を念頭に置いて作成されたいくつかの言語 (Whiley、Dafny、Frama-C など) の言語比較に取り組んでいます。ある配列の領域を別の配列にコピーし、コピー先内の配置が異なる関数のこの例を受け取りました。配列。私が思いついた仕様は、Dafny では次のようになります。
上記の 2 番目の while ループには、考えられるすべてを網羅しようとしたため、不要な不変条件が含まれている可能性があります。しかし、ええ、これは検証されておらず、その理由について当惑しています...
recursion - Dafny-recursiveSum アサーション違反
dafny で再帰的な sum 関数を書き、その正しさを証明しようとしました。私は書いた：
これは私が書いた証明です：
SUM1:
SUM2:
私が得るエラー：
理由を理解してください。
count - dafny の無効なセグメント数
以下のリンクのコードの次の証明を書きました。count2 メソッドの証明について助けを求めたいと思います。代替証明は私にはあまり明確ではありません ありがとう