Re: Instantiating package problems

[Andrew Shvets <andrew.shvets@gmail.com>]

On Wednesday, January 6, 2016 at 8:07:45 AM UTC-5, G.B. wrote:
> On 06.01.16 06:00, Andrew Shvets wrote:
> > On Tuesday, January 5, 2016 at 11:52:00 PM UTC-5, Anh Vo wrote:
> 
> >> The preconditions and postconditions are controlled by pragma Assertion_Policy. Thus, pragma Assertion_Policy(Check) must be added at the top of the package specification. Absent of this pragma is equivalent to pragma Assertion_Policy (Ignore). That means these conditions are ignored. By the way, ASSERTION_ERROR exception would be raised instead of CONSTRAINT_ERROR.
> >
> > This is how the body looks like now:
> > http://pastebin.com/Mt0E0HAD
> >
> > I'm still getting a constraint error.
> >
> 
> You should see something like this, after adding Assertion_Policy
> in the way Anh Vo has described:
> 
> raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from 
> shvets.ada:15
> 
> If you know that what Dmitry has explained is true,
> you could state it as a workable approximation,
> so that clients of the package know what to do when
> the programmers are not certain about all implications,
> practical and theoretical, of predefined division "/"
> in Input1/Input2, Integer'[Base']Range, and more:
> 
> 
>     Extra_Value : constant Boolean :=
>       not (Integer'Last = -Integer'First);
> 
>     function Division
>       (Input1 : in Integer;
>        Input2 : in Integer)
>       return Integer
>     with
>       Pre =>
>         Input2 /= 0
>         and
>         (if Extra_Value
>          then not (Input1 = Integer'First and Input2 = -1)),
>       Post =>
>         Input1/Input2 in Integer'Range
>         and
>         Division'Result = Input1/Input2;

It makes sense in principle.  I've seen something similar in erlang where you could check if one of the inputs is an integer, float, etc.