help / color / mirror / Atom feed
* Contracts in generic formal subprogram
@ 2023-04-08  7:00 mockturtle
  2023-04-08  8:02 ` Dmitry A. Kazakov
                   ` (2 more replies)
  0 siblings, 3 replies; 13+ messages in thread
From: mockturtle @ 2023-04-08  7:00 UTC (permalink / raw)

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?)
   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
       Pre => Is_Invertible (X);
   with function Gcd (X, Y : Ring) return Ring
       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?).


^ permalink raw reply	[flat|nested] 13+ messages in thread

end of thread, other threads:[~2023-04-13  6:27 UTC | newest]

Thread overview: 13+ messages (download: mbox.gz / follow: Atom feed)
-- links below jump to the message on this page --
2023-04-08  7:00 Contracts in generic formal subprogram mockturtle
2023-04-08  8:02 ` Dmitry A. Kazakov
2023-04-11  5:56   ` G.B.
2023-04-11 12:03     ` Dmitry A. Kazakov
2023-04-12  2:18       ` Spiros Bousbouras
2023-04-12  3:37         ` Spiros Bousbouras
2023-04-12  6:49           ` Niklas Holsti
2023-04-12  7:30           ` G.B.
2023-04-12 12:29           ` Ben Bacarisse
2023-04-13  6:27         ` Dmitry A. Kazakov
2023-04-08  9:09 ` Randy Brukardt
2023-04-08 16:48 ` Simon Wright
2023-04-08 17:27   ` mockturtle

This is a public inbox, see mirroring instructions
for how to clone and mirror all data and code used for this inbox