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?