問題タブ [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.
arrays - Dafny: 配列を入力する理由 Dafny はそれがシーケンスだと言っています
入力が配列であることは明らかですが、flag[1..] に進むと、flag がシーケンスであると表示されるのはなぜですか? リンクはこちら：http: //rise4fun.com/Dafny/fUgu
arrays - (Dafny) 配列で検索 - ゼロで囲まれたループバリアント?
配列a内の要素eを見つけようとする次のDafnyコードを検討してください。
検証は正常に機能しますが、よくわからないことがあります。間違いがなければ、ループのバリアントは、整数の場合、ゼロで区切られている必要があります。ただし、最後の反復ではu-iゼロを下回ります。i = u+1Dafny がu-iゼロに制限されていないことについて文句を言わないのはなぜですか?
dafny - 一連の整数の要素の合計: ループ不変式はループによって維持されない可能性があります
「Dafny 入門: ガイド」を読んだ後、最初のプログラムを作成することにしました。整数のシーケンスが与えられたら、その要素の合計を計算します。しかし、Dafny にプログラムを検証してもらうのに苦労しています。
私は得る
プログラムを検証するために、Dafny には何らかの「助け」が必要なのではないかと思います (レンマかな?) が、どこから始めればよいかわかりません。