From mboxrd@z Thu Jan  1 00:00:00 1970
X-Spam-Checker-Version: SpamAssassin 3.4.6 (2021-04-09) on
	ip-172-31-65-14.ec2.internal
X-Spam-Level: 
X-Spam-Status: No, score=-0.0 required=3.0 tests=BAYES_20,FREEMAIL_FROM,
	T_SCC_BODY_TEXT_LINE autolearn=ham autolearn_force=no version=3.4.6
X-Received: by 2002:a0c:c78b:0:b0:5df:47b4:a977 with SMTP id k11-20020a0cc78b000000b005df47b4a977mr1788797qvj.5.1680937238671;
        Sat, 08 Apr 2023 00:00:38 -0700 (PDT)
X-Received: by 2002:a25:d0c6:0:b0:b8e:c88b:23ec with SMTP id
 h189-20020a25d0c6000000b00b8ec88b23ecmr1320721ybg.10.1680937238418; Sat, 08
 Apr 2023 00:00:38 -0700 (PDT)
Path: eternal-september.org!feeder.eternal-september.org!1.us.feeder.erje.net!feeder.erje.net!usenet.blueworldhosting.com!diablo1.usenet.blueworldhosting.com!peer03.iad!feed-me.highwinds-media.com!news.highwinds-media.com!news-out.google.com!nntp.google.com!postnews.google.com!google-groups.googlegroups.com!not-for-mail
Newsgroups: comp.lang.ada
Date: Sat, 8 Apr 2023 00:00:38 -0700 (PDT)
Injection-Info: google-groups.googlegroups.com; posting-host=54.36.30.212; posting-account=9fwclgkAAAD6oQ5usUYhee1l39geVY99
NNTP-Posting-Host: 54.36.30.212
User-Agent: G2/1.0
MIME-Version: 1.0
Message-ID: <0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com>
Subject: Contracts in generic formal subprogram
From: mockturtle <framefritti@gmail.com>
Injection-Date: Sat, 08 Apr 2023 07:00:38 +0000
Content-Type: text/plain; charset="UTF-8"
Content-Transfer-Encoding: quoted-printable
X-Received-Bytes: 3293
Xref: feeder.eternal-september.org comp.lang.ada:65077
List-Id: <comp.lang.ada>

Dear.all,
this is something that looked like a natural and nice idea to me, but the c=
ompiler disagree :-): specifying contracts in formal subprograms in generic=
 declarations.  Actually,   RM 12.6 does not prohibit this on a syntactic l=
evel (a aspect_specification part is included), but the compiler complains.

To understand what I mean, please check the following real code toy-zed (ca=
n you hear the grammar screaming?)
-----------------------
generic
   type Ring is private;

   with function Divides (Num, Den : Ring) return Boolean;  =20
   with function Is_Invertible (X : Ring) return Boolean;  =20
   with function Inv (X : Ring) return Ring
     with
       Pre =3D> Is_Invertible (X);
  =20
   with function Gcd (X, Y : Ring) return Ring
     with
       Post =3D> Divides (X, Gcd'Result) and Divides (Y, Gcd'Result);=20
package Pippo is
   -- stuff
end Pippo;
----------------------------------
The meaning I have in mind is something like

* For "Pre" aspect: who writes function Inv  can assume that X is invertibl=
e since Inv will never be called (by the package code, at least) with X not=
 invertible.   Also Inv cannot have a stricter pre-condition.  In a sense, =
the package expects Inv to work correctly if and only if the pre-condition =
is true.

* For "Post" aspect: I expect that the result of GCD satisfies the post con=
dition.  Post conditions for the actual subprogram can be stricter, as long=
 as the post condition of the formal parameter is satisfied.  For example, =
if Ring is Integer, GCD could always return a positive value that divides b=
oth X and Y.  The fact that the result is positive does not hurt.

Should   the actual subprogram specify the same contract?  I am not sure (a=
nd I guess this could be a stumbling block for the adoption of this idea). =
 One could say that the actual subprogram gets a contract that is the AND o=
f the actual subprogram and the contract specified in the generic declarati=
on, it is up to the programmer to check that they are compatible.  I guess =
the compatibility could be verified by the compiler itself in simple cases,=
 but I expect that this could not be feasible in some cases (maybe of acade=
mic interest?).

Riccardo