Grammar clarifications, particularly \in and \subset

[davidcok]

Various grammar clarifications: precedence of \in and \subset; description of some potentially confusing points; some renaming for consistency.

[davidcok]

I added that update to a range of cells as a point of discussion. I consider it would be useful a) for initializing a whole array, as in { a \with [..] = 0 } And to extend even further, to use a lambda expression as in { a \with [m .. n ] = (\lambda int j ; j). }

These forms are helpful for describing the results of array manipulation in loops Of course quantified assertions can also be used, at the expense of being more verbose.

That said, in my current edits this line is marked experimental, and it is not critical.

• David

On Jul 11, 2019, at 1:30 PM, Virgile Prevosto notifications@github.com wrote:

@vprevosto commented on this pull request.

My only point is about the introduction of update to a range of cells.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/58?email_source=notifications&email_token=ABITDQF3YMZ6OAQUY4UCRM3P64KVZA5CNFSM4H24R6N2YY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOB6EPQVY#pullrequestreview-260634711, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQHFTIDPYQNSYHK7IW3P64KVZANCNFSM4H24R6NQ.

[vprevosto]

I agree that writing such terms is probably easier than a universal quantification. I was more concerned about what tools could do with that afterwards (especially the \lambda variant), but the ACSL manual is not supposed to worry too much about that. Still, I'd rather not have that in the basic terms but at a later stage.

[davidcok]

OK. Though loc.tex is about sets of locations so this definition does not seem to fit there.

• David

On Jul 11, 2019, at 4:34 PM, Virgile Prevosto notifications@github.com wrote:

I agree that writing such terms is probably easier than a universal quantification. I was more concerned about what tools could do with that afterwards (especially the \lambda variant), but the ACSL manual is not supposed to worry too much about that. Still, I'd rather not have that in the basic terms but at a later stage.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/58?email_source=notifications&email_token=ABITDQBFMFV5O7NVFGNOJOTP65AINA5CNFSM4H24R6N2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZW4W3Y#issuecomment-510511983, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQBWX6ZMIXF457SWEMLP65AINANCNFSM4H24R6NQ.

[davidcok]

Actually, I suggest omitting it here in the basic terms and instead adding a variant allowing lambda terms when lambdas are introduced under higher-order features.

• David

On Jul 11, 2019, at 4:39 PM, David Cok david.r.cok@gmail.com wrote:

OK. Though loc.tex is about sets of locations so this definition does not seem to fit there.

• David

On Jul 11, 2019, at 4:34 PM, Virgile Prevosto <notifications@github.com mailto:notifications@github.com> wrote:

I agree that writing such terms is probably easier than a universal quantification. I was more concerned about what tools could do with that afterwards (especially the \lambda variant), but the ACSL manual is not supposed to worry too much about that. Still, I'd rather not have that in the basic terms but at a later stage.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/58?email_source=notifications&email_token=ABITDQBFMFV5O7NVFGNOJOTP65AINA5CNFSM4H24R6N2YY3PNVWWK3TUL52HS4DFVREXG43VMVBW63LNMVXHJKTDN5WW2ZLOORPWSZGODZW4W3Y#issuecomment-510511983, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQBWX6ZMIXF457SWEMLP65AINANCNFSM4H24R6NQ.

[vprevosto]

Sounds good. I'll commit something in this direction.

[vprevosto]

OK, ranges are now in the tsets section and array slice updates in the higher-order one. While writing an example for the latter, I did notice that array initialization wasn't extremely well described in the document (section 2.2.7 merely indicates that we use C designated initializers syntax). I've added a sentence to indicate that it is possible to have ranges (and \lambdas as well) there too, but at some point having proper grammar entries for both the standard designated initialization and the range-based one would be desirable (maybe not in this PR, though).

[pbaudin]

That is ok for me and have only one question about the "functional update" & "offset extension" implemented into Frama-C. Do we add them into ACSL ?

[davidcok]

Patrick, The grammar in the manual does not accommodate this syntax at all.

Do you mean

{ a \with .c.[ range ] = 0 }

What syntax is actually implemented in current Frama-c? What is the ‘c’ in the above?

• David

On Jul 18, 2019, at 11:45 AM, P. Baudin notifications@github.com wrote:

@pbaudin commented on this pull request.

In term.tex https://github.com/acsl-language/acsl/pull/58#discussion_r304829036:

@@ -23,6 +23,7 @@ | term bin-op term ; | term "[" term "]" ; array access | "{" term "\with" "[" term "]" "=" term "}" ; array functional modifier

• | "{" term "\with" "[" range "]" "=" term "}" ; array functional modifier Sorry for the noice, array slice updates are implementated and the Frama-C transformation about the offset extension rejects correctly the previous exemple.

Good, every thing is ok with that. I noticed also that { a \with c.[ range ] = 0 } is accepted and transformed into { a \with c = { a.c \with [range] = 0 }}. That is correct.

— You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub https://github.com/acsl-language/acsl/pull/58?email_source=notifications&email_token=ABITDQAFNMB7BS5TZVW2YDLQAA3RZA5CNFSM4H24R6N2YY3PNVWWK3TUL52HS4DFWFIHK3DMKJSXC5LFON2FEZLWNFSXPKTDN5WW2ZLOORPWSZGOB62VZJA#discussion_r304829036, or mute the thread https://github.com/notifications/unsubscribe-auth/ABITDQDQPU6CWD663QIMIN3QAA3RZANCNFSM4H24R6NQ.

[pbaudin]

David, The implemented syntax for the offset in updates is the one you use in initializers. The Frama C implementation tranforms an update with a compound offset in several updates with elementary offsets (those described into the actual ACSL document). That eases the work of Frama-C plugins, but that transformation allows ranges only for the last offset. There is below an example accepted by Frama-C since a long time:

struct st_c { int t[10] ; int c ;} ;
//@ logic struct st_c update1_idx_in_field (struct st_c a, integer idx, int x) = { a \with .t[idx] = x };

struct st_b { struct st_c c ; };
//@ logic struct st_b update2_idx_in_field (struct st_b a, integer idx, int x) = { a \with .c.t[idx] = x };
//@ logic struct st_b update2_range_in_field (struct st_b a, integer idx, int x) = { a \with .c.t[0..idx] = x };

//@ type ST10 = struct st_c [10];
//@ logic ST10 update3_field_at_idx (ST10 a, integer idx, int x) = { a \with [idx].c = x };

Unfortunately, as said before, the next update is not implemented into Frama-C.

//@ logic ST10 update3_field_in_range (ST10 a, integer idx, int x) = { a \with [0..idx].c = x };
// [kernel:annot-error] exemple.i: Warning:  range is only allowed for last offset. Ignoring global annotation

It could be nice to add this extension into the ACSL document. It is up to you.

[vprevosto]

@pbaudin while I agree that allowing explicitly in the document a designator list instead of a single designator would be nice to have, I tend to think that this is relatively independent from this merge request (especially as the newly introduced range designators can only be put at the end of such a list). I'm thus inclined towards merging the current state and leaving designator lists for a later PR.