Using decl and def uniformly (and correctly)

[pbaudin]

1 The same kind of thing can be done for lemma in the "Figure: Grammar for global logic definitions".

2 For my point of you, its seems better to move axiom-def ::= ... from "Figure Grammar for axiomatic declarations" to "Figure Grammar for global logic definitions" even if axiom-def is used into logic-decl and not into logic-def. @davidcok, what is your point of you about that ?

[davidcok]

I would prefer that axiom-def be an instanceof logic-def and not logic-decl (and thereby be allowed to be written at global scope). Shall I make this change?

In fact I would prefer that all declarations be allowed at global scope. The user can combine them into an axiomatic when it makes sense to do so.

• David

On Wed, Jun 26, 2019 at 3:02 PM P. Baudin notifications@github.com wrote:

1. The same kind of thing can be done for lemma in the "Figure: Grammar for global logic definitions".

2 For my point of you, its seems better to move axiom-def ::= ... from "Figure Grammar for axiomatic declarations" to "Figure Grammar for global logic definitions" even if axiom-def is used into logic-decl and not into logic-def. @davidcok https://github.com/davidcok, what is your point of you about that ?

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/60?email_source=notifications&email_token=ABITDQDOQE3MEJLST3HLPLTP4NSENA5CNFSM4H3QKFX2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODYTOFDQ#issuecomment-505864846, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQAYCXY6XLMCYVSQXOTP4NSENANCNFSM4H3QKFXQ .

[pbaudin]

I don't think that axiom-def could be accepted at global scope. As far I can undertand, the motivation is the folowing: the axioms that belong to an axiomatic block define the footprint of the predicates/functions that are declared into the same block and use the defined footprint of the predicates/functions that are declared in others blocks. I will leave @vprevosto to give its feeling about that point.

[davidcok]

Yes I understand that is the rationale and recommended practice. However, there are circumstances in which a global axiom is convenient, perhaps about a built-in function — so I would prefer that the tool accept global axioms and declarations and leave it to the user to organize the specification for best understanding.

• David

On Jun 27, 2019, at 8:18 AM, P. Baudin notifications@github.com wrote:

I don't think that axiom-def could be accepted at global scope. As far I can undertand, the motivation is the folowing: the axioms that belong to an axiomatic block define the footprint of the predicates/functions that are declared into the same block and use the defined footprint of the predicates/functions that are declared in others blocks. I will leave @vprevosto https://github.com/vprevosto to give its feeling about that point.

— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/60?email_source=notifications&email_token=ABITDQAGHTIMV25J6PYSJADP4RLSHA5CNFSM4H3QKFX2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODYWB5ZQ#issuecomment-506207974, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQCCOL72TOHL3Q7EVXLP4RLSHANCNFSM4H3QKFXQ.

[vprevosto]

I tend to agree with @davidcok : we should not forbid axioms at toplevel. However, it would probably be useful to indicate explicitly that this is discouraged and that in a well structured specification, all axioms should belong to an axiomatic together with the functions/predicates they are defining.

[vprevosto]

Actually, it looks as though the main changes were already present in #58 . This PR is now reduced to a mere whitespace fix. No need to delay merging in those circumstances