0

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

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

テスト仕様:

with SPARK.Ada.Text_IO; use SPARK.Ada.Text_IO;

package test with SPARK_Mode
is

   continue_messages_key : Character := ' ';

   procedure User_Wait_For_Continue_Messages_Key
   with Global => (In_Out => Standard_Input,
                   Input => continue_messages_key),
        Pre => Is_Readable (Standard_Input) and then
                    not End_Of_File; 

end test;

試験体:

pragma SPARK_Mode(On);

package body test is

   procedure User_Wait_For_Continue_Messages_Key
   is
      IR : Immediate_Result;
      Avail : Boolean;
   begin
      loop
         Get_Immediate(IR, Avail);
         if Avail then
            if IR.Status = Success then
               if IR.Available = True then
                  if IR.Item = continue_messages_key then
                     return;
                  end if;
               end if;
            end if;
         end if;
      end loop;
   end User_Wait_For_Continue_Messages_Key;

end test;

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

procedure Get_Immediate (Item      :    out Character_Result)
     with Global => (In_Out => Standard_Input),
          Pre    => Is_Readable (Standard_Input) and then
                    not End_Of_File,
          Post   => Is_Readable (Standard_Input) and
                    Name (Standard_Input) = Name (Standard_Input)'Old and
                    Form (Standard_Input) = Form (Standard_Input)'Old and
                    Is_Standard_Input (Standard_Input);

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

4

1 に答える 1

2

特別なコメントの時代から SPARK を使用していないことから始めましょう。そのため、私の回答は現在の使用状況を反映していない可能性があります。

SPARK を見る 1 つの方法は、プログラムが遭遇する可能性のあるすべてのことについて考えさせるということです。前提条件が False の場合、プログラムは何をすべきでしょうか? この可能性を考慮したことを示さなければなりません。

Standard_Input でのすべての SPARK.Ada.Text_IO 操作に、Get_Immediate のように事後条件があるIs_Readable (Standard_Input)と仮定すると、次のようなものを配置するだけで十分です。

pragma Assert (Is_Readable (Standard_Input) );

プログラムの先頭に追加し、これをプロシージャ (および Standard_Input を読み取るその他のサブプログラム) の事後条件に追加します。次に、前提条件のその部分がプログラム全体で保持されていることを確認する必要があります。(SPARK が最初に Standard_Input が読み取り可能であることを保証する場合、アサーションは必要ないかもしれません。)

not End_Of_Fileはもう少し複雑です。少なくとも一部のプラットフォームでは、False になる可能性があります。たとえば Linux では、Ctrl-D を行の最初に入力すると EOF として扱います。パイプまたは入力リダイレクトから読み取っている場合もあります。ループ中にユーザーが EOF に入ると、 End_Of_File が True のときにプロシージャが Get_Immediate を呼び出すことがあります。おそらく、この部分を手順の前提条件から外して、体を次のように変更する必要があります

All_Chars : loop
   if not End_Of_File then
      Get_Immediate (IR, Avail);

      exit All_Chars when Avail               and then
                          IR.Status = Success and then
                          IR.Available        and then
                          IR.Item = Continue_Messages_Key;
   end if;
end loop All_Chars;

次に、Get_Immediate の前提条件が満たされ、End_Of_File が True になると明らかに望ましい動作 (無限ループ) が得られることを確認します (その場合、IR の一部のフィールドがチェックの 1 つに失敗すると仮定します)。

あなたのコードには不可解な点がいくつかあります。まず、グローバル変数です。グローバル変数は諸悪の根源であり、少なくとも読み取り不能なコードを保証します。次に、手順の特異性があります。もっと一般的なものではないでしょうか

procedure Wait_For_Key (Key : in Character);

書いて証明するのが同じくらい簡単で、より便利ですか？次に、ネストされた if ステートメントの文字列があります。これは、 に接続された同等の条件よりも読みにくいと思いますand then。最後に、Boolean と True の比較があります。「=」はブール値を返すので、「=」の左側に既にあるブール値が必要であることを示しているのではないでしょうか?

おそらく、「=」の結果も True と比較する必要があることを意味します。次に、その "=" の結果も True と比較する必要があります。これは、これを書いている人が決して終わらないことを保証するので、より良いかもしれません.

于 2017-11-17T14:45:15.547 に答える