From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.4 (2020-01-24) on polar.synack.me
X-Spam-Level: 
X-Spam-Status: No, score=-0.3 required=5.0 tests=BAYES_00,
	REPLYTO_WITHOUT_TO_CC autolearn=no autolearn_force=no version=3.4.4
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!.POSTED!not-for-mail
From: "G.B." <bauhaus@futureapps.invalid>
Newsgroups: comp.lang.ada
Subject: Re: Instantiating package problems
Date: Wed, 6 Jan 2016 14:07:43 +0100
Organization: A noiseless patient Spider
Message-ID: <n6j3e0$51q$1@dont-email.me>
References: <7dcd49f3-b04f-4ea3-b431-5c27f73b9afe@googlegroups.com>
 <87poxixqmy.fsf@theworld.com>
 <b5dcba43-8652-40f0-8115-a235c6c83544@googlegroups.com>
 <f2fabc7b-a6a4-49db-85ac-d0fedf6cf95e@googlegroups.com>
 <112f5e6c-35c1-483a-b8dd-24f5f76dc6ce@googlegroups.com>
 <084197af-8e37-4250-a083-b45bd9ab4609@googlegroups.com>
 <e35407bf-554e-4075-a4d8-18f63f784817@googlegroups.com>
Reply-To: nonlegitur@futureapps.de
Mime-Version: 1.0
Content-Type: text/plain; charset=windows-1252; format=flowed
Content-Transfer-Encoding: 7bit
Injection-Date: Wed, 6 Jan 2016 13:05:04 -0000 (UTC)
Injection-Info: mx02.eternal-september.org;
 posting-host="b96887e80893c84a90c3007226ca0d1c";
	logging-data="5178"; mail-complaints-to="abuse@eternal-september.org";
	posting-account="U2FsdGVkX1+jiM9llk3q0MhBlpD4iIlHwN5/ODp21U0="
User-Agent: Mozilla/5.0 (Macintosh; Intel Mac OS X 10.10; rv:38.0)
 Gecko/20100101 Thunderbird/38.5.0
In-Reply-To: <e35407bf-554e-4075-a4d8-18f63f784817@googlegroups.com>
Cancel-Lock: sha1:Vynht1xvwqu7a6iDtaZ+fQeKhhM=
Xref: news.eternal-september.org comp.lang.ada:29032
Date: 2016-01-06T14:07:43+01:00
List-Id: <comp.lang.ada>

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;