"Assertion might Fail" and Precondition doesn't solve it

Question

I have a function that monitors a controlled signal by applying a simple check whether the signal is within a given tolerance band. The function is called is_within_limits. I have a second function called is_within_expanded_limits that does the same but applies an expansion factor (widens the tolerance band) to the configured limits beforehand. The limits are configured in monitor.config by means of a target value and a maximum deviation from that value or lower and upper thresholds. The enumeration monitor.config.monitoring_mode specifies how the valid range is specified.

Have a look at the code first.

Specification

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;

Implementation

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;

My problem is that the assertion pragma Assert (expanded_lower_threshold < expanded_upper_threshold) is marked as might fail and I don't understand why. I added that assertion to check that my code does nothing weird like inverting the relation of lower and upper threshold but primarily to try out assertions. The precondition monitor.config.lower_threshold < monitor.config.upper_threshold in conjunction with the code that calculates expanded_lower_threshold and expanded_upper_threshold should guarantee that the assertion always holds true. Where is the problem and how can I fix it?

Answer 1

My conjecture is that your provers simply ran into a timeout. I tried your example and that is what happend to me.

Usually, the user interface is not distinguishing between different causes of failing proofs. If you run into a timeout and don't notice, then it makes it look like something is wrong with your code, although it maybe isn't. Since you must be using GNATprove (there is no other tool at the moment), go into your build folder and look for a subfolder called "gnatprove". There, you will find a file called your_package_name.spark. This is a JSON format, which gives you information what the provers really reported. I am sure you will find a timeout or step limit there. I think your code might be defect-free, as I will substantiate in a minute.

But first of all, your code is not compiling. You have to use a proper type to define the range of parameter signal_value in function is_within_expanded_limits. Since the range is the same, you could use Float_Signed1000. Alternatively, add a precondition (but the type is better, since then also callers that are not in SPARK_Mode get some type/range checking).

Then, consider changing the comparison to "<=", since it might be possible that rounding errors refute a strict ordering. I am not sure whether this is problematic in this case, but be aware that SPARK models IEEE754-compliant computations, and there it can make a difference whether you have a number 1.2 (which cannot be precisely represented), or 1.25 (which can). Thus, I made this little change to your code.

Now back to my claim that your code could be correct despite failing proofs. Add this to the top of your case:

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

Warning: don't use assume pragmas other than for figuring out why a proof fails. Things can go horribly wrong if they are used incorrectly.

Now select the slowest mode for verification, and your assertion checks out (the prover has less "cominations" to check). You can change the value in the assume statement as you like, but be careful that the value is agreeing with type ranges and precondition, otherwise everything gets proven wrongfully (e.g., try Float'Last, and then place a pragma assert (False) immediately after the assume). If something does not get proven, go and see why as described above. There is no point in changing your code before you know that the prover actually came to a conclusion.

You can try out the SPARK lemma library, which can enable these kind of stubborn proofs: http://www.spark-2014.org/entries/detail/gnatprove-tips-and-tricks-using-the-lemma-library