1

您好，我正在尝试从此函数编写证明注释..这是使用 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.
4

3 回答 3

2

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

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

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

两个小的旁注：

  • 请使用与语言参考手册中相同的标识符样式。（前导大写，下划线分隔单词。）
  • 为什么是Sensor_Index_Type的子类型Integer？
于 2013-11-18T09:12:54.060 回答
1

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

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

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

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

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

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

于 2013-11-18T09:48:54.940 回答
0

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

消息：
The identifier count1 is either undeclared or not visible at this point.
似乎表明情况确实如此。

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

于 2013-11-17T22:14:33.503 回答