問題タブ [proofs]
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.
16 問題
0
投票する
1
に答える
451
参照
ada - 二重ループに埋め込まれた関数で Ada/SPARK 前提条件を証明する方法
以下のプログラムの実行中に「prepend」の前提条件が成立することを証明しようとしています。前提条件は次のとおりです。
これを証明するための私の試みは、プラグマの形式で以下のコードにあります。この前提条件が 1 つのループには当てはまることを証明できますが、2 つのループには当てはまりません。非常に複雑なループ不変条件の例は見つかりましたが、二重ループの例は見つかりません。
仕様:
体：
エラーは「ループ不変式は最初の反復で失敗する可能性があり、Illumination_Sources_Pkg.Length(Illumination_Sources) <= X*Y を証明できません」です。最初の反復後に失敗する可能性があるとは言っていないので、それは何かです。