Spark Proof annotation

Question

hello I am trying to write proof annotations from this function .. this is written using the Spark programming language

function Read_Sensor_Majority return Sensor_Type is
       count1:Integer:=0;
       count2:Integer:=0;
       count3:Integer:=0;

      overall:Sensor_Type;

   begin


      for index in Integer range 1..3 loop
         if State(index) = Proceed then
           count1:=count1+1;
         elsif State (index) = Caution then
            count2:=count2+1;
         elsif State (index)=Danger then
            count3:=count3+1;
         end if;
      end loop;

      if count1>=2 then
         overall:=Proceed;
      elsif count2>=2 then
         overall:=Caution;
      elsif count3>=2 then
         overall:=Danger;
      else
         overall:=Undef;
      end if;

      return overall;

   end Read_Sensor_Majority;

   begin -- initialization
   State:= Sensordata'(Sensor_Index_Type => Undef);
end Sensors;

---

this is the .ads file

package Sensors
   --# own State;
   --# initializes State;
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;
   --# derives State from State ,Value_1, Value_2, Value_3;

   function Read_Sensor(Sensor_Index: in Sensor_Index_Type) return Sensor_Type;
   --# global in State;

   function Read_Sensor_Majority return Sensor_Type;
   --# global in State;
   --# return overall => (count1>=2 -> overall=Proceed) and
   --#                   (count2>=2 -> overall=Caution) and
   --#                   (count3>=2 -> overall=Danger);


end Sensors;

these are the errors I am getting after examining the file using the spark examiner

Examiner Semantic Error   1 - The identifier count1 is either undeclared or not visible at this point. <b>34:27</b>     Semantic Error   1 - The identifier count1 is either undeclared or not visible at this point. Examiner
Sensors.ads:34:27
Semantic Error   1 - The identifier count1 is either undeclared or not visible at this point.

Answer 1

You have to declare identifiers before you can reference them (with some exceptions).

Most important of all, it is a basic principle in both SPARK and Ada that specifications can be processed without any knowledge whatsoever of possible matching implementations.

As neither overall, nor count1, count2 or count3 are declared in the specification, you can't reference them there either.

Two small side notes:

• Please use the same identifier style as in the language reference manual. (Leading upper-case, underscores separating words.)
• Why is Sensor_Index_Type a subtype of Integer?

Answer 2

Just playing with SPARK myself so this is not a complete answer.

(It's worth mentioning which SPARK as there are different versions and SPARK-2014 seems to be quite a bit different from the others) I currently only have the 2006 edition of Barnes which doesn't cover the latest versions.

The basic problem is quite obvious : having provided an abstract view of the package's state --# own State; in the spec, you cannot then reach in and observe the specifics.

What to do about it is not completely clear to me, but has the outline form: provide a more abstract form of the postconditions for Read_Sensor_Majority in the specification, and move the concrete form to the body.

One approach adopted in Ada-2012 (I don't know how applicable to Spark-2005) is to provide an additional function in the spec function satisfies_conditions (...) return boolean; which can be called in the annotations, and whose body contains the concrete implementation.

Barnes (ed. above) p.278 does show "proof functions" which can be declared in the annotations for this purpose. Their bodies then have access to the internal state to perform the concrete checks.

Answer 3

Given that you are showing the .ads and .adb files, I note that the proof in the .ads file is referencing items in the body. Could it be that the prover cannot reach into the body and pull these variables? (i.e. an issue of visibility.)

The message:
The identifier count1 is either undeclared or not visible at this point.
Seems to indicate that this is the case.

I don't know SPARK, so that's my best-guess.