問題タブ [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.

0 投票する
1 に答える
180 参照

dafny - Dafny 命名規則の制御と定数の使用

Dafny がターゲット コードに使用する命名規則を制御する方法はありますか?

シンボリック定数をグローバルに使用することは可能ですか? このようなもの:

数値式を文字列に変換する方法はありますか?

0 投票する
1 に答える
519 参照

dafny - ネストされたループのインデックス範囲外エラー

このコードが「範囲外のインデックス」エラーを生成する理由を誰か教えてもらえますかinput[i*cols + j]?

0 投票する
1 に答える
75 参照

arrays - 配列のコピーでソースを変更しようとしています

配列のスライスを別のスライスにコピーする次のコードでは、ソース配列が保持されることを示すループ不変式は検証されません。

これはthis questionthis other oneに関連していますが、この場合に機能するものはまだ見つかりません。