0

我有一个功能，通过应用一个简单的检查信号是否在给定的容差范围内来监控受控信号。该函数被调用is_within_limits。我有第二个函数is_within_expanded_limits，它的作用相同，但事先将扩展因子（扩大公差带）应用于配置的限制。monitor.config通过目标值和与该值的最大偏差或下限和上限阈值来配置限制。枚举monitor.config.monitoring_mode指定如何指定有效范围。

先看一下代码。

规格

subtype Float_Signed1000 is Float range -1_000.0 .. 1_000.0;
subtype Float_Signed10000 is Float range -10_000.0 .. 10_000.0;

type Monitor_Config_T is record
   monitoring_mode : Monitoring_Mode_T := mean_based;

   mean : Float_Signed1000 := 0.0;
   maximum_deviation : Float range Float'Small .. 1_000.0 := 100.0e-3;
   lower_threshold : Float_Signed1000 := -100.0e-3;
   upper_threshold : Float_Signed1000 := 100.0e-3;

   settling_tolerance_expansion : Float range (1.0 + Float'Small) .. 2.0 := 1.2;

   startup_time : Time_Span := Milliseconds (5);
   settling_time : Time_Span := Milliseconds (2);
   violation_time : Time_Span := Milliseconds (5);
   retry_time : Time_Span := Milliseconds (100);
end record;

type Monitor_T is record
   config : Monitor_Config_T;
   timer : Time_Span := Milliseconds (0);
   current_state : Monitor_State_T := reset;
   next_state : Monitor_State_T := reset;
end record;

function is_within_expanded_limits (monitor : in Monitor_T; 
                                 signal_value : in Float_Signed1000) 
                                 return Boolean
  with Pre => (if monitor.config.monitoring_mode = mean_based then
                 monitor.config.maximum_deviation > 0.0)
              and then (if monitor.config.monitoring_mode = threshold_based then
                           monitor.config.lower_threshold < 
                               monitor.config.upper_threshold)
              and then monitor.config.settling_tolerance_expansion > 1.0;

执行

function is_within_expanded_limits (monitor : in Monitor_T; 
                                  signal_value : in Float_Signed1000) 
                                  return Boolean is
     within_expanded_limits : Boolean := False;

     expanded_lower_threshold : Float Float_Signed10000;
     expanded_upper_threshold : Float Float_Signed10000;
begin
   case monitor.config.monitoring_mode is
      when mean_based =>
         if abs (monitor.config.mean - signal_value) <= 
            (monitor.config.maximum_deviation * 
                monitor.config.settling_tolerance_expansion) then
           within_expanded_limits := True;
        end if;

      when threshold_based =>
         --  Added due to recommendation by Jacob Sparre Andersen
         --  Assertion is proved successfully
         --  pragma Assert (monitor.config.lower_threshold < monitor.config.upper_threshold);

         --  Added due to recommendation by Martin Becker
         --  Adding this assumption still causes the assertion to fail
         --  pragma Assume (monitor.config.lower_threshold = 10.0);

         --  Adding this assumption still causes the assertion to fail
         --  pragma Assume (monitor.config.upper_threshold = 11.0);

         --  Replacing the assumption with this one results in the assertion being proved
         --  pragma Assume (monitor.config.upper_threshold = 20.0);

         --  Calculate expanded thresholds
         if monitor.config.lower_threshold >= 0.0 then
            expanded_lower_threshold := monitor.config.lower_threshold / 
                monitor.config.settling_tolerance_expansion;
         else
            expanded_lower_threshold := monitor.config.lower_threshold * 
               monitor.config.settling_tolerance_expansion;
         end if;

         if monitor.config.upper_threshold >= 0.0 then
            expanded_upper_threshold := monitor.config.upper_threshold * 
               monitor.config.settling_tolerance_expansion;
         else
            expanded_upper_threshold := monitor.config.upper_threshold / 
               monitor.config.settling_tolerance_expansion;
         end if;

         --  @TODO why does this assertion fail?
         pragma Assert (expanded_lower_threshold < expanded_upper_threshold);

         --  Check limits with expanded thresholds
         if signal_value >= expanded_lower_threshold and signal_value <= 
             expanded_upper_threshold then
            within_expanded_limits := True;
         end if;
   end case;

   return within_expanded_limits;

end is_within_expanded_limits;

我的问题是断言pragma Assert (expanded_lower_threshold < expanded_upper_threshold)被标记为可能失败，我不明白为什么。我添加了该断言以检查我的代码是否没有像反转下阈值和上限阈值的关系那样奇怪，但主要是为了尝试断言。先决条件monitor.config.lower_threshold < monitor.config.upper_threshold与计算代码的结合expanded_lower_threshold应expanded_upper_threshold保证断言始终成立。问题出在哪里，我该如何解决？

4

1 回答 1

1

我的猜想是你的证明者只是遇到了超时。我试过你的例子，这就是发生在我身上的事情。

通常，用户界面不会区分证明失败的不同原因。如果您遇到超时并且没有注意到，那么它会使您的代码看起来有问题，尽管它可能不是。由于您必须使用 GNATprove（目前没有其他工具），请进入您的构建文件夹并查找名为“gnatprove”的子文件夹。在那里，您会找到一个名为 your_package_name.spark 的文件。这是一种 JSON 格式，可以为您提供证明者真实报告的信息。我相信你会在那里找到超时或步数限制。我认为您的代码可能没有缺陷，我将在一分钟内证实这一点。

但首先，您的代码没有编译。您必须使用正确的类型来定义 function 中参数 signal_value 的范围is_within_expanded_limits。由于范围相同，您可以使用Float_Signed1000. 或者，添加一个前提条件（但类型更好，因为那时不在 SPARK_Mode 中的调用者也会进行一些类型/范围检查）。

然后，考虑将比较更改为“<=”，因为舍入错误可能会反驳严格的排序。我不确定在这种情况下这是否有问题，但请注意，SPARK 对符合 IEEE754 的计算进行建模，并且无论您有数字 1.2（无法精确表示）还是 1.25（可以），都会有所不同. 因此，我对您的代码做了一些小改动。

现在回到我的主张，即尽管证明失败，您的代码可能是正确的。将此添加到案例的顶部：

pragma Assume (monitor.config.lower_threshold = 10.0);

警告：除了找出证明失败的原因之外，不要使用假设编译指示。如果使用不当，事情可能会大错特错。

现在选择最慢的验证模式，并且您的断言检查出来（证明者需要检查的“组合”更少）。您可以根据需要更改假设语句中的值，但请注意该值与类型范围和前提条件一致，否则一切都会被错误地证明（例如，尝试Float'Last，然后pragma assert (False)在假设之后立即放置 a）。如果某些事情没有得到证实，请按照上述说明去看看原因。在您知道证明者实际上得出结论之前更改您的代码是没有意义的。

您可以试用 SPARK 引理库，它可以启用这些顽固的证明：http ://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-using-the-lemma-library

于 2018-01-31T13:51:20.823 回答