問題タブ [spark-2014]

スペース文字である文字列内の最初の文字を見つけて、そのインデックスを返すにはどうすればよいContract_Casesですか?

たとえば、文字列が次の場合:

式は を返す必要があり4ます。

以下のプログラムの実行中に「prepend」の前提条件が成立することを証明しようとしています。前提条件は次のとおりです。

これを証明するための私の試みは、プラグマの形式で以下のコードにあります。この前提条件が 1 つのループには当てはまることを証明できますが、2 つのループには当てはまりません。非常に複雑なループ不変条件の例は見つかりましたが、二重ループの例は見つかりません。

仕様:

体：

エラーは「ループ不変式は最初の反復で失敗する可能性があり、Illumination_Sources_Pkg.Length(Illumination_Sources) <= X*Y を証明できません」です。最初の反復後に失敗する可能性があるとは言っていないので、それは何かです。

SPARK Discovery 2017 の spark_io の例から SPARK.Text_IO を使用しています。

私の問題は、多くの SPARK.Text_IO プロシージャに、標準入力が読み取り可能であり、ファイルの終わりではないことを証明する方法がわからないという前提条件があることです。以下のコードに示されているように、私の試みは、SPARK.Text_IO プロシージャ (この場合は Get_Immediate) の前提条件を呼び出し元のプロシージャの前提条件に追加することでした。 . うまくいきませんでした。これが私が話していることの例です：

テスト仕様:

試験体:

証明者が与えるエラーは、Get_Immediate の行「中: 前提条件が失敗する可能性があります」にあります。

Standard_Input が読み取り可能であり、ファイルの終わりではないことを SPARK にどのように証明しますか?

私はフレームワーク Frama-c を研究していますが、C/Frama-c と Spark Ada の間に同等性があるかどうか疑問に思っています。このような異なる言語を比較するのは非常に奇妙に思えるかもしれませんが、David A. Wheeler の記事、Johannes Kanig の比較、および SPARK のユーザーマニュアルを少し読んだ後、SPARK と C/Frama-c/ACSL が与えるかどうかを推測するのに苦労しています。同じ証明の堅牢性と同じコードの信頼性。

あなたの視点/経験を与えてくれてありがとう！

PS: 私は frama-c を初めて使用し、SPARK プログラミングについてあまり知りません。