Re: Contracts in generic formal subprogram

["Randy Brukardt" <randy@rrsoftware.com>]

Ada 2022 allows such contracts; Ada 2012 did not. (See 6.1.1, and 
specifically 6.1.1(1/5)). Whether your compiler has caught up, who knows.

Logically the contracts should "match" (with the weakening/strengthing that 
Dmitry mentioned), but that was too hard for Ada, so they're just additive. 
(A proper matching mechanism is more the sort of thing that SPARK does, Ada 
only enforces these contracts at runtime) That is, when you call through a 
generic formal subprogram, you enforce the preconditions of both the formal 
and the actual subprogram, and similarly for the postconditions. If they 
mismatch, you might not be able to make a successful call. If it hurts, 
don't do that. ;-)

                     Randy.


"mockturtle" <framefritti@gmail.com> wrote in message 
news:0c555ce7-0b2e-49f1-8930-c4f4796793e4n@googlegroups.com...
Dear.all,
this is something that looked like a natural and nice idea to me, but the 
compiler disagree :-): specifying contracts in formal subprograms in generic 
declarations.  Actually,   RM 12.6 does not prohibit this on a syntactic 
level (a aspect_specification part is included), but the compiler complains.

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

   with function Divides (Num, Den : Ring) return Boolean;
   with function Is_Invertible (X : Ring) return Boolean;
   with function Inv (X : Ring) return Ring
     with
       Pre => Is_Invertible (X);

   with function Gcd (X, Y : Ring) return Ring
     with
       Post => Divides (X, Gcd'Result) and Divides (Y, Gcd'Result);
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 invertible 
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 
condition.  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 both 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 
(and 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 of 
the actual subprogram and the contract specified in the generic declaration, 
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 academic 
interest?).

Riccardo