typo improvements for CH. 1

[davidcok]

Miscellaneous phrasing improvements to Sulfur Foreword & Ch. 1.

[vprevosto]

waiting for @davidcok feedback

[vprevosto]

The current implementation in Frama-C even requires the entire contract to be in the same comment. I'll propose something in this regard.

[vprevosto]

@davidcok you didn't provide a reference for OpenJML. Is the site OK or do you prefer the OpenJML article mentioned there?

[vprevosto]

@davidcok does it answer your remark?

[davidcok]

I will add an OpenJML link - or review the one you have added. Regarding contracts and extent of comments - we should distinguish what the langue states and what the current implementation requires, if we decide they should be different. - David From: Virgile Prevosto <notifications@github.com> To: acsl-language/acsl <acsl@noreply.github.com> Cc: David Cok <cok@frontiernet.net>; Mention <mention@noreply.github.com> Sent: Thursday, March 1, 2018 6:04 PM Subject: Re: [acsl-language/acsl] typo improvements for CH. 1 (#29) @vprevosto commented on this pull request.waiting for @davidcok feedbackIn intro_modern.tex:> or more occurrences of $e$, $e^+$ for repetition of one or more occurrences of $e$, and $e^?$ for zero or one occurrence of $e$. For the sake of simplicity, we only describe annotations in the usual \lstinline|/*@ ... */| style of comments. One-line annotations -in \lstinline|//@| comments are alike. - +in \lstinline|//@| comments are similar. +\marginpar{Somewhere it needs to be defined in what way ACSL specifications can be split across consecutive \lstinline|//@| comments, if they can be split at all. For example, JML requires each function contract clause to be completely within an annotation.} The current implementation in Frama-C even requires the entire contract to be in the same comment. I'll propose something in this regard.In biblio.bib:> @@ -8,6 +8,11 @@ @misc{ESCJava2 note = {\url{http://kind.ucd.ie/products/opensource/ESCJava2/}} } +@misc{OpenJML, @davidcok you didn't provide a reference for OpenJML. Is the site OK or do you prefer the OpenJML article mentioned there?In intro_modern.tex:> or more occurrences of $e$, $e^+$ for repetition of one or more occurrences of $e$, and $e^?$ for zero or one occurrence of $e$. For the sake of simplicity, we only describe annotations in the usual \lstinline|/*@ ... */| style of comments. One-line annotations -in \lstinline|//@| comments are alike. - +in \lstinline|//@| comments are similar. Note however that two consecutive @davidcok does it answer your remark?— You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or mute the thread.

[davidcok]

Regarding annotations: so must an entire function contract be in one annotation comment?  What about multiple loop invariants?Regarding bibliography - I added some references in the jmlupdate branchOn Mar 1, 2018, at 6:04 PM, Virgile Prevosto <notifications@github.com> wrote:@vprevosto commented on this pull request.waiting for @davidcok feedbackIn intro_modern.tex:

or more occurrences of $e$, $e^+$ for repetition of one or more

occurrences of $e$, and $e^?$ for zero or one occurrence of $e$. For the sake of simplicity, we only describe annotations in the usual \lstinline|/*@ ... */| style of comments. One-line annotations -in \lstinline|//@| comments are alike. - +in \lstinline|//@| comments are similar. +\marginpar{Somewhere it needs to be defined in what way ACSL specifications can be split across consecutive \lstinline|//@| comments, if they can be split at all. For example, JML requires each function contract clause to be completely within an annotation.} The current implementation in Frama-C even requires the entire contract to be in the same comment. I'll propose something in this regard. In biblio.bib:

@@ -8,6 +8,11 @@ @misc{ESCJava2

note = {\url{http://kind.ucd.ie/products/opensource/ESCJava2/}} } +@misc{OpenJML, @davidcok you didn't provide a reference for OpenJML. Is the site OK or do you prefer the OpenJML article mentioned there? In intro_modern.tex:

or more occurrences of $e$, $e^+$ for repetition of one or more

occurrences of $e$, and $e^?$ for zero or one occurrence of $e$. For the sake of simplicity, we only describe annotations in the usual \lstinline|/*@ ... */| style of comments. One-line annotations -in \lstinline|//@| comments are alike. - +in \lstinline|//@| comments are similar. Note however that two consecutive @davidcok does it answer your remark?—You are receiving this because you were mentioned.Reply to this email directly, view it on GitHub, or mute the thread. {"api_version":"1.0","publisher":{"api_key":"05dde50f1d1a384dd78767c55493e4bb","name":"GitHub"},"entity":{"external_key":"github/acsl-language/acsl","title":"acsl-language/acsl","subtitle":"GitHub repository","main_image_url":"<a href="https://cloud.githubusercontent.com/assets/143418/17495839/a5054eac-5d88-11e6-95fc-7290892c7bb5.png" class="">https://cloud.githubusercontent.com/assets/143418/17495839/a5054eac-5d88-11e6-95fc-7290892c7bb5.png</a>","avatar_image_url":"<a href="https://cloud.githubusercontent.com/assets/143418/15842166/7c72db34-2c0b-11e6-9aed-b52498112777.png" class="">https://cloud.githubusercontent.com/assets/143418/15842166/7c72db34-2c0b-11e6-9aed-b52498112777.png</a>","action":{"name":"Open in GitHub","url":"<a href="https://github.com/acsl-language/acsl" class="">https://github.com/acsl-language/acsl</a>"}},"updates":{"snippets":[{"icon":"PERSON","message":"@vprevosto commented on #29"}],"action":{"name":"View Pull Request","url":"<a href="#29 (review)" class="">#29 (review)</a>"}}}

[vprevosto]

Regarding annotations: so must an entire function contract be in one annotation comment? What about multiple loop invariants?

A function contract must indeed be in one annotation comment. It's the same thing for loop annotations: there can only be a single one for each loop, and it must encompass all loop invariants and loop assigns related to the loop.

Regarding bibliography - I added some references in the jmlupdate branch

OK, thanks

By the way, It seems that you made your comment by replying to the notification email you received, but I'm under the impression that github.com and your mailer do not cooperate very well, which makes your comment slightly difficult to read.

[vprevosto]

(forgot to answer this remark, sorry)

Regarding contracts and extent of comments - we should distinguish what the langue states and what the current implementation requires, if we decide they should be different.

Even though it was never explicitly mentioned, the fact that an ACSL annotation should fit entirely in a single comment has always been taken for granted. I'd suggest to keep the new clarification. If someone ever claims that they absolutely need to be able to split a contract/loop annotation into several comment, we might revise this option (of course, this person can be you 😁).