| 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"
|
Relationships 
Relationships