SPARK.Text_IO手順の前提条件は、私が2017年</p> <p>私の問題SPARKの発見にspark_io例からSPARK.Text_IOを使用してい

Question

を開催することを証明する方法はSPARK.Text_IO手順の多くは、前提条件を持っていることであるIどのようにして証明しようとするのかわからない、すなわち標準入力が読み込み可能であり、ファイルの終わりではないということです。私の試みは、以下のコードに示されているように、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; 

テスト本体：前提条件があります

証明者が与えエラーがGet_Immediateライン上にある」メディアが

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に証明しますか？

Answer 1

私は特別なコメントの日からSPARKを使用していないと言って始めましょう、私の答えは現在の使用法を反映していないかもしれません。

SPARKを調べる1つの方法は、プログラムが遭遇する可能性があるすべてのことを考えるようにすることです。前提条件が偽であれば、あなたのプログラムはどうすべきですか？あなたはこの可能性を考慮したことを示す必要があります。

Get_Immediateが、それはあなたのプログラムの冒頭で

pragma Assert (Is_Readable (Standard_Input)); 

のようなものを置くために十分とにこれを追加する必要がないようStandard_Input上のすべてのSPARK.Ada.Text_IO操作が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を呼び出すことがあります。そうでないと、SPARKはそれ以外の点では証明できません。おそらくあなたは、あなたの手順の前提オフこの部分を取り、次にあなたが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; 

のようなものにあなたの体を変更し、明らかに望ましい行動（無限ループ）の場合を持っている必要がありますEnd_Of_FileはTrueになります（この場合、IRの一部のフィールドがあなたのチェックの1つに失敗したと仮定します）。

あなたのコードについていくつか困惑していることがあります。最初に、グローバル変数があります。グローバル変数はAll Evilのルートであり、少なくともコードを読むことはできません。次に、手順の特異性があります。

procedure Wait_For_Key (Key : in Character); 

もっと一般的なものではないでしょうか？もっと簡単に書くことができ、より有用でしょうか？次に、ネストされたif文の文字列があります。これは、and thenに接続された同等の条件よりも読みにくいものです。最後に、BooleanとTrueを比較します。 "="はブール値を返すので、 "="の左側に既にあるブール値が必要であることを示していませんか？

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