search

acsl-language / acsl

Sources for the ANSI/ISO C Specification Language manual
Other
49 stars 8 forks source link

typo improvements for CH. 1 #29

Closed davidcok closed 6 years ago

davidcok commented 6 years ago

Miscellaneous phrasing improvements to Sulfur Foreword & Ch. 1.

davidcok commented 6 years ago

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.

@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 commented 6 years ago

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":"https://cloud.githubusercontent.com/assets/143418/17495839/a5054eac-5d88-11e6-95fc-7290892c7bb5.png","avatar_image_url":"https://cloud.githubusercontent.com/assets/143418/15842166/7c72db34-2c0b-11e6-9aed-b52498112777.png","action":{"name":"Open in GitHub","url":"https://github.com/acsl-language/acsl"}},"updates":{"snippets":[{"icon":"PERSON","message":"@vprevosto commented on #29"}],"action":{"name":"View Pull Request","url":"https://github.com/acsl-language/acsl/pull/29#pullrequestreview-100501917"}}}

vprevosto commented 6 years ago

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 commented 6 years ago

(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 😁).