火花证明注释

Question

您好，我正在尝试使用此函数编写证明注释.. 这是使用 Spark 编程语言编写的

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;

---

这是 .ads 文件

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;

这些是我使用 spark 检查器检查文件后遇到的错误

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

您必须先声明标识符，然后才能引用它们（有一些例外）。

最重要的是，在 SPARK 和 Ada 中的一个基本原则是，可以在不知道任何可能匹配实现的情况下处理规范。

由于规范中既没有声明overall，也没有声明count1、count2 或count3，因此您也不能在那里引用它们。

两个小注：

• 请使用与语言参考手册中相同的标识符样式。 （前导大写，下划线分隔单词。）
• 为什么Sensor_Index_Type 是Integer 的子类型？

Answer 2

我自己只是在玩 SPARK，所以这不是一个完整的答案。

（值得一提的是哪个SPARK，因为有不同的版本，SPARK-2014似乎与其他版本有很大不同）我目前只有Barnes的2006版，不包括最新版本。

基本问题非常明显：在规范中提供了包状态--# own State; 的抽象视图，然后您无法进入并观察细节。

我对此并不完全清楚，但有大纲形式： 为规范中的 Read_Sensor_Majority 提供更抽象的后置条件形式，并将具体形式移至正文。

在 Ada-2012 中采用的一种方法（我不知道如何适用于 Spark-2005）是在规范中提供一个附加功能 function satisfies_conditions (...) return boolean; 可以在注释中调用，其主体包含具体实现.

Barnes (ed. above) p.278 确实显示了“证明函数”，可以为此目的在注释中声明。然后他们的身体可以访问内部状态来执行具体的检查。

Answer 3

鉴于您正在显示 .ads 和 .adb 文件，我注意到 .ads 文件中的证明引用了正文中的项目。会不会是证明者无法伸入体内并拉出这些变量？ （即可见性问题。）

留言：
The identifier count1 is either undeclared or not visible at this point.
似乎表明是这样的。

我不知道 SPARK，所以这是我的最佳猜测。