search

AdaCore / ada-spark-rfcs

Platform to submit RFCs for the Ada & SPARK languages
63 stars 28 forks source link

[RFC] Possibly not returning procedure calls #30

Closed yannickmoy closed 4 years ago

yannickmoy commented 4 years ago

Link to full text: https://github.com/yannickmoy/ada-spark-rfcs/blob/possibly_not_returning/considered/possibly_not_returning.rst

sttaft commented 4 years ago

Seems like a good solution to the problem. Could define a new aspect some day if this becomes a widely used capability. -Tuck

sshyamsunder1988 commented 4 years ago

Thanks Yannick. I think the proposal looks good.

However I do have a question regarding the writeup: 1) Only procedures can be "Possibly_Not_Returning" right? However No_Return aspect can be given for a function. For example: The scenario I am thinking of is the following: Function A is No_Return. Procedure B is "Possibly_Not_Returning" and procedure B calls Function A. This is a valid scenario right?

clairedross commented 4 years ago

I think No_Return is already only allowed for procedures. As a possible extension, we could consider adding the boolean expression of ACSL if we need something more precise one day. For proof, we would generate an additional postcondition that the boolean no_return is equal to this expression.

yannickmoy commented 4 years ago

@sshyamsunder1988 no only a procedure can be marked No_Return

sshyamsunder1988 commented 4 years ago

@sshyamsunder1988 no only a procedure can be marked No_Return

I see. I was mistaken then. Thanks for confirming Yannick and Claire.

Regards Shreyas

clairedross commented 4 years ago

We should take care with dispatching calls. On tagged overidding of procedures, would have to force this pragma to match on the overridden and overriding primitives. How does it work for pragma No-Return currently?

sttaft commented 4 years ago

On Wed, Oct 16, 2019 at 5:34 AM Claire Dross notifications@github.com wrote:

We should take care with dispatching calls. On tagged overidding of procedures, would have to force this pragma to match on the overridden and overriding primitives. How does it work for pragma No-Return currently?

In RM 6.5.1(6/5-7/5):

6/5 A subprogram shall be nonreturning if it overrides a dispatching nonreturning subprogram. In addition to the places where Legality Rules normally apply (see 12.3), this rule applies also in the private part of an instance of a generic unit.

7/5 If a renaming-as-body completes a nonreturning subprogram declaration, then the renamed subprogram shall be nonreturning.

For possibly-non-returning, it would seem that at least in SPARK the opposite should apply. If a subprogram that overrides a dispatching subprogram is marked as possibly-non-returning, then the subprogram it overrides should also be marked as possibly-non-returning. Alternatively, you could have a separate rule, where a dynamically dispatching call is presumed to always be possibly non returning, unless there is a promise that it is not possibly non returning, purpose with a separate notion of, say, possibly-non-returning'Class.

For Ada, the goal was to be sure No_Return is not lying, but we don't require that all non-returning subprograms be declared as such. In SPARK, I would think that you want to have a No_Return exactly when the subprogram is non returning. So the overriding rules in SPARK will probably need to be stricter, or we'll need some notion of No_Return'Class.

-Tuck

— You are receiving this because you commented. Reply to this email directly, view it on GitHub, or unsubscribe.

yannickmoy commented 4 years ago

thanks @sttaft for pointing out the rule for non-returning subprograms. Actually in SPARK we could allow overridding with both directions of change without impacting soundness, at least in theory. In practice it will be cumbersome to handle mixed cases in derivations, for no visible benefit, so I'd rather impose the same policy on all overriddings of a primitive.

yannickmoy commented 4 years ago

what about a simpler name for the annotation like May_Not_Return (closer to No_Return) rather than Possibly_Not_Returning?

clairedross commented 4 years ago

what about a simpler name for the annotation like May_Not_Return (closer to No_Return) rather than Possibly_Not_Returning?

I like it.

sttaft commented 4 years ago

"May not" is ambiguous in English. I would recommend "Might_Not_Return" instead.

-Tuck

On Wed, Oct 30, 2019 at 11:46 AM Claire Dross notifications@github.com wrote:

what about a simpler name for the annotation like May_Not_Return (closer to No_Return) rather than Possibly_Not_Returning?

I like it.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/30?email_source=notifications&email_token=AANZ4FIV3DMQ6DGECJEWGE3QRGT35A5CNFSM4I6ETSNKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOECUWQXY#issuecomment-547973215, or unsubscribe https://github.com/notifications/unsubscribe-auth/AANZ4FODVXU6QJDYLEZDYDLQRGT35ANCNFSM4I6ETSNA .

sttaft commented 4 years ago

As indicated in another reply, "may not" is ambiguous in English, meaning either "must not" or "might not." Hence, I would recommend "Might_Not_Return" if you want a (slightly) shorter name. It is fewer syllables, at least! ;-) -Tuck

On Wed, Oct 30, 2019 at 11:43 AM yannickmoy notifications@github.com wrote:

what about a simpler name for the annotation like May_Not_Return (closer to No_Return) rather than Possibly_Not_Returning?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/AdaCore/ada-spark-rfcs/pull/30?email_source=notifications&email_token=AANZ4FKICZSWJN55EO6GMN3QRGTT3A5CNFSM4I6ETSNKYY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGOECUWIVQ#issuecomment-547972182, or unsubscribe https://github.com/notifications/unsubscribe-auth/AANZ4FNBJTDFO4WPRSPBSYDQRGTT3ANCNFSM4I6ETSNA .