問題タブ [spark-ada]

私は非常に単純なプログラムを書きましたが、それが機能的に正しいことを証明できませんでした。アイテムのリストを使用し、各アイテムには無料か使用済みかを示すフィールドがあります。

使用された要素の数を示すカウンターもあります。

append_itemプロシージャは、used_items カウンターをチェックして、リストがいっぱいかどうかを確認します。そうでない場合は、最初の空きエントリが使用済みとしてマークされ、used_itemsカウンターがインクリメントされます。

used_itemsがリスト内の使用済み要素の数と等しいことを証明する方法がわかりません。また、gnatprove のメッセージは時々不可解であり、多くの gnatprove/* ファイルのどこで詳細情報を探すべきかわからないことにも注意してください。実際、私にとっての主な困難は、証明者が何を必要としているのかを理解することです。以上のことについて、何かご指摘がありましたら幸いです。

引数 (Ada.Command_Line.Argument) と GetLine からの入力が有効であることを確認するための簡単な検証コード ブロックを作成しようとしています。私の場合、入力文字列のすべての文字が数字 (0 から 9 ）。

main.adb:

test_procedure.ads:

test_procedure.adb

プログラムは完全に正常に動作します。入力./main 01234すると が返さaaaaaれ、入力./main f00しても何も返されません。ただし、GNATprove (GPS -> SPARK -> Prove All) を使用すると、precondition might fail, cannot prove S(I) >= '0' (e.g. when I = 1 and user_str = (2 => '0', others => 'NUL')). 数字がない文字が存在する場合、ToA プロシージャを呼び出すべきではないため、なぜこのようなことが起こるのかわかりません。

次のようなおおよそのデータ構造があります (完全なソースを共有することはできませんが、要求に応じて追加情報を提供できます)。

完全なコードはエラーや警告なしでコンパイルされますが、SPARK の証明ステップは次のエラーで失敗します。

SPARK マニュアルの対応する部分を読みましたが、それらに従ってコードを修正する方法がわかりません。ティア。