Ada design by contracts critical software

Question

I have a question related to applying contracts in a critical environment.

Imagine I have the following function to divide:

function div (dividend, divisor : Float) return Float
with Pre => divisor /= 0;

Well, for me the pre-condition is part of the signature of the function and every client must be aware of the contract, if a client pass a zero to the divisor argument is its fault bacause he is violating the contract and thus the function will fail. In testing, with pre-conditions activated, the code will fail showing a contract violation and, in production with pre-conditions deactivated, would fail raising a constraint.

As a constraint error is not acceptable in a critical environment, this is what the client is requiring me for the implementation, to call a module that manages inconsistencies:

function div (dividend, divisor : Float) return Float is
begin
  if divisor = 0 then
    InconsistencyManager.inconsistency ("Some Log"); --It firstly logs a message and then does an infinite loop
  end;

  return dividend / divisor; --If everything is ok, return the division
end div;

For me this side effect for a function its quite weird, and for me violating a contract is like passing the wrong type to a subprogram, the difference is that this kind of error is caught at compilation time and the contract violation, if there aren't enough tests, could stop the execution of the program when is already installed.

Do you really has to protect against human stupidity like this? Do you really has to penalize the function execution making always that question?

Answer 1

What your client requires you to do -- to check preconditions within the subprogram, then call an "inconsistency manager" -- is IMO the old-fashioned way. If the inconsistency occurs and leads to an infinite loop, what happens to the "critical system"? Crash and burn? Or is there a redundant system that can take over? That does not always work well, as shown for example by the Ariane 501 launch failure where both hot-redundant computers met with the same "inconsistency", and predictably so.

The old-fashioned way is also a beast to unit-test for complete coverage.

IMO the way to go today is to have a Precondition, as in your first code example, and then use a prover -- CodePeer, SPARK, GNATprove -- to prove once and for all, ahead of execution, that the precondition is never violated (barring HW error, but if you expect HW errors your critical system has bigger problems).

However, if your actual code really has floating-point parameters, do note that testing the divisor for (exactly) equal to zero (0.0) does not prevent all overflows. You need some smarter numerical analysis to check what the precondition should actually be, taking into account both the divisor and the dividend.

Answer 2

You are not required to use a precondition to achieve your desired goal. You can use a static_predicate to define the subtype for the divisor parameter.

with Ada.Text_IO; use Ada.Text_IO;

procedure subtype_test is
   epsilon : constant float := 0.00001;
   subtype divisor_type is float with
     static_predicate => divisor_type not in -epsilon .. epsilon;
   function div (dividend : float; divisor : divisor_type) return float is
   begin
      return dividend / divisor;
   end div;

   divisors : array (1 ..2) of float := (0.1, 0.0);
   dividend : float := 10.0;

begin
   for value of divisors loop
      if value in divisor_type then
         Put_Line("Result: " & float'Image(div(dividend, value)));
      else
         Put_Line("Logging error -> Divisor equals 0.0");
      end if;
   end loop;
end subtype_test;

In this case the calling subprogram must check for correctness of the divisor and perform the error logging instead of calling the div function. The use of a subtype as shown above allows the calling subprogram to easily check the validity of the parameters before calling the div function.