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
--- SoupGate-Win32 v1.05
* Origin: fsxNet Usenet Gateway (21:1/5)