問題タブ [spark-ada]

InefficientEuler1Sum と InefficientEuler1Sum2 の 2 つの関数があります。両方が同等であることを証明したい (同じ入力に対して同じ出力)。SPARK -> Prove File (GNAT Studio 内) を実行するpragma Loop_Invariant(Sum = InefficientEuler1Sum(I));と、ファイル euler1.adb の行に関する次のようなメッセージが表示されます。

1. loop invariant might fail in first iteration
2. loop invariant might not be preserved by an arbitrary iteration

関数 InefficientEuler1Sum2 は InefficientEuler1Sum の構造について何も知らないようです (たとえば、手動で証明しようとすると)。この情報を提供する最良の方法は何ですか?

ファイル euler1.ads:

ファイル euler1.adb:

ドキュメントとコードを検索してみましたが、これが何であるかを見つけることができないため、修正方法がわかりません。

シナリオ：

私は Ada SPARK ベクトル ライブラリを使用しており、次のコードがあります。

コードが呼び出すとエラーが発生します：

を指していEmpty_Vectorます。難しいのは、問題を引き起こしているように見えるasをEmpty_Vector定義することです。今では、型定義にあるように見えるので、それをどのように処理するかわかりません( を調べました)。Capacity0Capacitya-cofove.ads

したがって、基本的に私はこれを解決する方法について行き詰まっています。または、これが将来起こることをどのように見つけるか。

私の問題の概要

SHA256 関数にlibsparkcrypto ライブラリを使用しています。私はそれが意味することができないAssertことを発見しています。どんな助けでも大歓迎です。x = ySha256(x) = Sha256(y)

コード

テストパッケージ.adb

testpackage.ads

出力

私が受け取るエラーは次のとおりです。

testpackage.adb:8:25: 中: アサーションが失敗する可能性があり、LSC.SHA2.Hash_SHA256 (X) = LSC.SHA2.Hash_SHA256 (Y) を証明できません [考えられる説明: testpackage.ads:8 のサブプログラムで X と Y を指定する必要があります前提条件][#0]

私のgnatprove.out：

私は Ada noob であり、整数のリストを取り、各要素を 1 ずつ減らす単純な関数を作成しています。私のブロンズ モードの証明は問題ありませんが、実際にメインで関数を使用して、実際に何をしているかを確認しようとしています。闘争を証明することになっています。配列を初期化して値を割り当てる方法がわかりません（0..10であるはずです）。また、decrement(integer) 関数と decrementList(ArrayOfNumbers) 関数ではなく、1 つの decrement 関数だけでこれを実装できたかどうかもわかりません。または、私がそれを正しく行っている場合。私が見つけた良いドキュメントがないので、自分の道を推測することになっているように感じます。このパッケージは、以前のタスクの一部であるため、flip_coin と呼ばれます。コインの反転に関連するものは無視できます。

仕様ファイルは次のとおりです。

本体ファイルは次のとおりです。

ここにメインファイルがあります：

実行しようとしたときのエラーは次のとおりです。

どんな助けでも大歓迎です。ティア