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=-1.9 required=5.0 tests=BAYES_00,FREEMAIL_FROM
	autolearn=unavailable autolearn_force=no version=3.4.4
X-Received: by 10.182.255.203 with SMTP id as11mr96798369obd.49.1452141743400;
        Wed, 06 Jan 2016 20:42:23 -0800 (PST)
X-Received: by 10.182.227.200 with SMTP id sc8mr281937obc.0.1452141743370;
 Wed, 06 Jan 2016 20:42:23 -0800 (PST)
Path: 
 eternal-september.org!reader01.eternal-september.org!reader02.eternal-september.org!news.eternal-september.org!mx02.eternal-september.org!feeder.eternal-september.org!news.glorb.com!h5no941794igh.0!news-out.google.com!l1ni6006igd.0!nntp.google.com!h5no941793igh.0!postnews.google.com!glegroupsg2000goo.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Wed, 6 Jan 2016 20:42:23 -0800 (PST)
In-Reply-To: <n6j3e0$51q$1@dont-email.me>
Complaints-To: groups-abuse@google.com
Injection-Info: glegroupsg2000goo.googlegroups.com;
 posting-host=2601:18f:900:8350:ba86:87ff:fed6:5907;
 posting-account=3pYsyQoAAACcI-ym7XtMOI2PDU8gRZS5
NNTP-Posting-Host: 2601:18f:900:8350:ba86:87ff:fed6:5907
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>
 <n6j3e0$51q$1@dont-email.me>
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <690510c8-f5ed-4bcf-b937-f65ef293f23c@googlegroups.com>
Subject: Re: Instantiating package problems
From: Andrew Shvets <andrew.shvets@gmail.com>
Injection-Date: Thu, 07 Jan 2016 04:42:23 +0000
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: quoted-printable
Xref: news.eternal-september.org comp.lang.ada:29041
Date: 2016-01-06T20:42:23-08:00
List-Id: <comp.lang.ada>

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:
>=20
> >> The preconditions and postconditions are controlled by pragma Assertio=
n_Policy. Thus, pragma Assertion_Policy(Check) must be added at the top of =
the package specification. Absent of this pragma is equivalent to pragma As=
sertion_Policy (Ignore). That means these conditions are ignored. By the wa=
y, 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.
> >
>=20
> You should see something like this, after adding Assertion_Policy
> in the way Anh Vo has described:
>=20
> raised SYSTEM.ASSERTIONS.ASSERT_FAILURE : failed precondition from=20
> shvets.ada:15
>=20
> 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:
>=20
>=20
>     Extra_Value : constant Boolean :=3D
>       not (Integer'Last =3D -Integer'First);
>=20
>     function Division
>       (Input1 : in Integer;
>        Input2 : in Integer)
>       return Integer
>     with
>       Pre =3D>
>         Input2 /=3D 0
>         and
>         (if Extra_Value
>          then not (Input1 =3D Integer'First and Input2 =3D -1)),
>       Post =3D>
>         Input1/Input2 in Integer'Range
>         and
>         Division'Result =3D Input1/Input2;

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