Re: Instantiating package problems

["G.B." <bauhaus@futureapps.invalid>]

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;