1

私はSPARKアプローチでAdaの自動列車保護を行っています。これはSPARKでの私の仕様です：

package Sensors
--# own State,Pointer,State1,State2;
--# initializes State,Pointer,State1,State2;
  is
    type Sensor_Type is (Proceed, Caution, Danger, Undef);
       subtype Sensor_Index_Type is Integer range 1..3;


  procedure Write_Sensors(Value_1, Value_2, Value_3: in Sensor_Type);
  --# global in out State,Pointer;
  --# derives State from State,Value_1, Value_2, Value_3,Pointer &
  --#                        Pointer from Pointer;
  function Read_Sensor(Sensor_Index: in Sensor_Index_Type) return Sensor_Type;

  function Read_Sensor_Majority return Sensor_Type;

  end Sensors;

これが私のエイダです：

   package body Sensors is
      type Vector is array(Sensor_Index_Type) of Sensor_Type;
      State: Vector;

      Pointer:Integer;
      State1:Sensor_Type;
      State2:Sensor_Type;

      procedure Write_Sensors(Value_1, Value_2, Value_3: in Sensor_Type) is
      begin
         State(Pointer):=Value_1;
         Pointer:= Pointer + 1;
         State(Pointer):=Value_2;
         Pointer:= Pointer + 1;
         State(Pointer):=Value_3;
      end Write_Sensors;

      function Read_Sensor (Sensor_Index: in Sensor_Index_Type) return Sensor_Type
      is
         State1:Sensor_Type;
      begin
         State1:=Proceed;
         if  Sensor_Index=1 then
            State1:=Proceed;
         elsif Sensor_Index=2 then
            State1:=Caution;
         elsif Sensor_Index=3 then
            State1:=Danger;
         end if;
         return State1;
      end Read_Sensor;

      function Read_Sensor_Majority return Sensor_Type is
         State2:Sensor_Type;      
      begin
         State2 := state(1);
         return State2;
      end Read_Sensor_Majority;

   begin -- initialization
      State:=Vector'(Sensor_Index_Type =>Proceed);  
      pointer:= 0; 
      State1:=Proceed;
      State2:=Proceed;
   end Sensors;

関数Read_Sensor_MajorityでState（1）またはState（）配列値を使用できない理由を知りたいです。それらを使用する方法がある場合、それを実現するためにSPARKの仕様に何かを入れる必要がありますか？

表示されているエラーは次のとおりです。

1)Expression contains referenced to variable state which has an undefined value flow error 20
2)the variable state is nether imported nor defined flow error 32
3)the undefined initial value of state maybe used in the derivation of the function value flow error 602
4

2 に答える 2

2

読むにはスペックを変更する必要があります

function Read_Sensor_Majority return Sensor_Type;
--# global in State;

上記のコメントで言ったように、私は戸惑いました

State := Vector'(Sensor_Index_Type => Proceed);

しかし、コンパイラはそれを受け入れるので、それはOKでなければなりません。そして、少しのテストはそれがと同じ効果を持っていることを示しています

State := Vector'(others => Proceed);

また、SPARKGPL2011ツールセットがMacOSXで利用できるようになったことをお知らせします。

于 2011-11-15T20:01:27.963 に答える
0

ふふ。まあ、それらは間違いなく「庭の多様性」コンパイラエラーではなく、SPARKエラーです。

単なる不完全な文字起こしではなく、エラーの実際のカットアンドペーストバージョン（およびそれらが参照している行の表示）を確認すると便利です。ただし、セキュリティ/接続性の理由から、これが常に可能であるとは限りません。

3つすべてが、システムを介したデータの流れについて不満を言っているようです。それらがどの行を参照しているかわからない場合、私が提案できる最善の方法は、システム内のデータの流れを手動でトレースして、それらの問題が何であるかを確認することです。

State(1)ここにある情報を大胆に推測する必要がある場合は、ルーチンからの値の読み取りに問題がある可能性がありRead_Sensor_Majorityます。これは、以前に値を配置したことを知る方法がないためです。そのアレイの場所に。

begin...endSimonがコメントで指摘したように、パッケージ自体にコンパイルエラーがあるように見えることを除いて、パッケージの本体領域にあるコードはそれを処理する必要があります。おそらく、その問題を修正すると、SPARKは何が起こっているのかを理解し、制御フローについての不満をやめます。

SPARKがAdaコンパイラを通過しないコードで「混乱している」エラーを吐き出すのが好きな場合は、SPARKにコードを確認する前に、Adaコンパイラがコードの純粋なAda部分を気に入っていることを確認するのが賢明かもしれません。以上。

于 2011-11-15T14:24:25.333 に答える