View Issue Details [ Jump to Notes ] | [ Issue History ] [ Print ] | ||||||||
ID | Project | Category | View Status | Date Submitted | Last Update | ||||
---|---|---|---|---|---|---|---|---|---|
0002115 | Frama-C | Documentation > ACSL | public | 2015-05-05 17:36 | 2016-01-26 08:52 | ||||
Reporter | dcok@grammatech.com | ||||||||
Assigned To | patrick | ||||||||
Priority | normal | Severity | minor | Reproducibility | have not tried | ||||
Status | closed | Resolution | fixed | ||||||
Product Version | Frama-C Sodium | ||||||||
Target Version | Frama-C Magnesium | Fixed in Version | Frama-C Magnesium | ||||||
Summary | 0002115: Typos and Grammatical corrections for the ACSL 1.9 manual | ||||||||
Description | These are a set of typos and grammatical errors I noted on a recent read of most of the ACSL 1.9 manual. None of these affect technical correctness - just the flow of the English. I put them here simply to be helpful. Do what you like with them. If you like, I am happy to edit them into a version-controlled copy of the document source myself, if you would like. Typos & Grammatical corrections p.13: "used in position of a term or a predicate" -> "used in the position of a term or a predicate" p. 17: "name x for expression e1 which can be used in" -> "name x for expression e1 ; x can then be used in" p. 17: "for readibility purposes" -> "for readability purposes" p. 20, near end: "specified if divisor is" -> "specified if the divisor is" p. 23: "involve any rounding nor overflow" -> "involve any rounding or overflow" p. 23: "values which do not naturally" -> "values that do not naturally" p. 23: "mode in C programs) If the source real number" -> "mode in C programs). If the source real number" (period added) p. 26: "pointers can only refers" -> "pointers can only refer" p. 27: "functional update of an union. For an object of an union" -> "functional update of a union. For an object of a union" p. 27: "Then equality amounts the recursively check equality of fields." -> "Then equality amounts to recursively checking equality of fields." p. 27: "C aggregates types" -> "C aggregate types" p. 28: "only for arrays that lies in C" -> "only for arrays that lie in C" p. 28: Did you intentionally omit the section on string literals? (2.2.8) p. 29, last line: "Thus, \old construct is useless" -> "Thus, the \old construct is useless" (2 changes) p. 30: "denotes the effective parameter of isqrt calls which" -> "denotes the effective parameter of isqrt calls, which" (comma expected here) p. 30: "in the pre-state than in the post-state" -> "in the pre-state as in the post-state" p. 33: "If such a condition is seeked," -> "If such a condition is desired," p. 34: "which are also usefull for \separated predicate" -> "that are also useful for the \separated predicate" (three changes) p. 38: "that are not member of L." -> "that are not members of L." p. 38: "is similar as above" -> "is similar to the above" p. 38, Remarks: "locations that are not member of L" -> "locations that are not members of L" p.43, last line: "but without decreases clause" -> "but without a decreases clause" p. 44: "the begining of the annoted statement" -> "the beginning of the annotated statement" (two changes) p. 47, last line: "These declarations follows the" -> "These declarations follow the" p. 49, Example 2.39: "The following introduce" -> "The following introduces" p. 50: "was also bases on definite Horn clauses thus consistent" -> "was also based on definite Horn clauses, and is thus consistent" (2 changes) p. 51: "there is no syntactic conditions which would" -> "there is no syntactic conditions that would" p. 52, Example 2.43: "Function that sums the element" -> "Function that sums the elements" p. 54: "C types and logic types arguments" -> "C type and logic type arguments" or "C types and logic types as arguments" p. 54: "Such an hybrid predicate" -> "Such a hybrid predicate" p. 54: "an hybrid function" -> "a hybrid function" p. 55, Example 2.46: "This second example defines a predicate which indicates" -> "This second example defines a predicate that indicates" p. 55, Example 2.46: "one of the post condition" -> "one of the post conditions" p. 55, "Logic declaration can be augmented" -> "Logic declarations can be augmented" p. 55: "of an hybrid" -> "of a hybrid" p. 56: "that is the set of memory locations which it depends on. From such an information" -> "that is, the set of memory locations that it depends on. From such information" (3 changes) p. 57: "Grammar for terms and predicates" -> "The grammar for terms and predicates" p. 57, at end of page: '(when the allocation succeed)" -> "(when the allocation succeeds)" p. 58, at top of page: "All of them takes" -> "All of them take" or "Each of them takes" p. 58, near bottom of page: "if there is no alignment constraints" -> "if there are no alignment constraints" p. 59: "in the post-state than in the pre-state" -> "in the post-state as in the pre-state" p. 61: "none of the two allocation clauses" -> "neither of the two allocation clauses" p. 61: "That is equivalent to give allocates \nothing" -> "That is equivalent to stating allocates \nothing" p. 63: "A loop-clause without allocation clause implicitly contents loop allocates \nothing" -> "A loop-clause without an allocation clause implicitly states loop allocates \nothing" (2 changes) p. 64: "since union is made with a" -> "since the arguments of union are a" p. 64: "accordingly to" -> "according to" p. 65: "abrupt clause of a statement contracts" -> "abrupt clause of statement contracts" p. 65: "e.g the value" -> "e.g. the value" (period added) p. 72, near end: "semantical restrictions" -> "semantic restrictions" p. 73: "execution This implies several conditions, including e.g:" -> "execution. This implies several conditions, including e.g.:" (two periods added) p. 73: "Body of a ghost function is ghost code, hence do not modify" -> "The body of a ghost function is ghost code, and hence may not modify" p. 74: "so as the ghost field of structures" -> "as do the ghost fields of structures" p. 79: "functions and predicate over" -> "functions and predicates over" p. 80, near end: "the pointer in argument is" -> "the pointer in the argument is" p. 83: "in the future, and remain open" -> "in the future and remain open" (no comma) p. 85: "The set of pure expression is a subset" -> "The set of pure expressions is a subset" | ||||||||
Tags | No tags attached. | ||||||||
Attached Files |
|
![]() |
|
signoles (manager) 2015-05-05 17:43 |
Thanks a lot for your so careful reading. We will fix them in the next public release. |
signoles (manager) 2015-06-09 16:56 |
Fixed, except the question about string literals (2.2.8). |
patrick (developer) 2015-09-07 13:45 |
Removing section bout string literals (2.2.8) |
![]() |
|||
Date Modified | Username | Field | Change |
---|---|---|---|
2015-05-05 17:36 | dcok@grammatech.com | New Issue | |
2015-05-05 17:36 | dcok@grammatech.com | Status | new => assigned |
2015-05-05 17:36 | dcok@grammatech.com | Assigned To | => signoles |
2015-05-05 17:43 | signoles | Note Added: 0005912 | |
2015-05-05 17:43 | signoles | Assigned To | signoles => virgile |
2015-05-05 17:43 | signoles | Target Version | => Frama-C Magnesium |
2015-05-12 13:26 | signoles | Assigned To | virgile => maroneze |
2015-06-09 16:56 | signoles | Assigned To | maroneze => virgile |
2015-06-09 16:56 | signoles | Note Added: 0005937 | |
2015-09-04 10:57 | bobot | Assigned To | virgile => patrick |
2015-09-07 13:45 | patrick | Note Added: 0006025 | |
2015-09-07 13:45 | patrick | Status | assigned => resolved |
2015-09-07 13:45 | patrick | Resolution | open => fixed |
2016-01-26 08:51 | signoles | Fixed in Version | => Frama-C Magnesium |
2016-01-26 08:52 | signoles | Status | resolved => closed |
2016-06-21 14:11 | signoles | Category | Documentation => Documentation > ACSL |