tset issues in manual "acsl-implementation-Aluminium-20160501.pdf"
ID0002236: This issue was created automatically from Mantis Issue 2236. Further discussion may take place here.
| Id | Project | Category | View | Due Date | Updated |
|---|---|---|---|---|---|
| ID0002236 | Frama-C | Documentation > manuals | public | 2016-06-27 | 2019-07-17 |
| Reporter | Jochen | Assigned To | patrick | Resolution | fixed |
| Priority | normal | Severity | text | Reproducibility | N/A |
| Platform | - | OS | - | OS Version | - |
| Product Version | - | Target Version | - | Fixed in Version | - |
Description :
in fig.2.7 on p.35, the alternative for set comprehension should be "{ term | binders ..." rather than " tset | binders ... ". The next line's alternative should also use "term" rather than "tset". In the corresponding explanation for set comprehension, probably not "the union of the sets denoted by s" is meant but rather "the set of all terms denoted by s".
When the rule "location-address ::= tset" is shown on p.58 and 79, and "location ::= tset" on p.29 (BTW: I wonder whether both rules should be joined into a single one?), some remark could be given on the semantics of (a singleton containing just) a proper-expression term. For example, "assigns n*n" seems perfectly valid, when "n" is an integer variable - are such clauses forbidden, or do they have a reasonable meaning?
On p.93, in the subsection "Typing rules for sets", rule 4 and 5 appear to deviate from the syntactical form explained at subsection start. There is no \vdash in the antecedent of rule 4, and no comma right of a \vdash in any of the involved 4 lines. In rule 5's antecedent, "b \cup \Lambda" should probably read "b:bool \cup \Lambda". I also didn't understand what "tset \tau" should mean.
In Fig.2.25 on p.72, no initialisation of a model variable is admitted by the grammar (since the rule "parameter ::= type-expr id", appearing on p.49 in Fig.2.12, dosn't allow an initialization), while in example 2.61 on p.73, the model variable "forbidden" is initialized, and apparently by a tset, viz. "\empty".