Ada and SPARK identifier `State` is either undeclared or not visible at this point

Question

I am doing an automatic train protection on Ada with SPARK approach. This is my spec in 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;

and this is my Ada:

   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;

I want to know why in the function Read_Sensor_Majority I can't use the State(1) or any of the State() array values. If there is a way to use them, should I put anything in the specs of SPARK to make it happen?

The errors it's showing are:

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

Answer 1

You need to change the spec to read

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

As I said in the comments above, I was puzzled by

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

but the compiler accepts it so it must be OK. And a little test shows that it has the same effect as

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

Also pleased to report that the SPARK GPL 2011 toolset is now available for Mac OS X!

Answer 2

Heh. Well, those are definitely SPARK errors, rather than "garden variety" compiler errors.

It would be nice to see an actual cut-and-paste version of the errors (along with an indication of which lines they are referring to) rather than just an imperfect transcription. However, I do realise that isn't always possible for security/connectivity reasons.

It looks like all three are complaining about the flow of data through your system. Without knowing which lines they refer to, the best I can suggest is to try to manually trace your flow of data through your system to try to see what their problem is.

If I had to take a wild guess with the info I have here, I'd say it perhaps has a problem with your reading of a value from State(1) in the routine Read_Sensor_Majority, because it has no way of knowing that you've previously placed a value into that array location.

The code you have in the package's begin...end body area should take care of that, except it appears to have a compile error itself, as Simon pointed out in the comments. Perhaps if you fix that problem, SPARK will understand what is going on and quit complaining about your control flows.

If SPARK likes to spit out "I'm confused" errors on code that doesn't even get past the Ada compiler, it might be wise to make sure the Ada compiler likes the pure Ada part of your code before asking SPARK to look it over.