Re: Preconditions which anyway would be caught?

[mockturtle <framefritti@gmail.com>]

On Saturday, August 9, 2014 5:35:21 PM UTC+2, Victor Porton wrote:
> function Inverse (X: Float) is
> 
> begin
>    return 1/X;
> end
>    with Pre => (X /= 0);
> 
> Is this precondition superfluous? (it anyway could be caught by erroneous 
> 1/X operation)

Still not a LL... I would say it is not.  It depends on the "reason" for specifying the precondition.  As I see it, the precondition is a kind of "formal documentation" of the conditions that must be satisfied when you call the function.  As a side effect, you can have those conditions checked at run-time as a "bug trap," but, for example, they could be used by some formal checking software.  So, even if calling the function with X=0 will cause an error, I would keep the precondition.

Riccardo