Group L.1 Issues
Issues
LRM (editorial) items: issues
62, 70, 71,
72, 73, 80,
87, 97, 104,
135.
Discussion
LRM Changes
-
4.2.2 Keywords:
add to Table 1--Keywords the following: bit, bitvector, for, numeric, string.
-
5.2.2 Informal Semantics, par. 2, first line:
change expression "a -> b" to be in "code" font.
-
5.2.3 Built-in functions
- Move the definition of Value_Set from 6.2.3, syntax 6-76, p91 to 5.2.3 Syntax-5.20, page 38.
- Replace Value_List by Value_Set in the following places:
- the syntax production for built-in function 'nondet' (5.2.3, syntax 5-20, p38)
- the syntax production for built-in function 'nondet_vector' (5.2.3, syntax 5-20, p38)
-
5.2.3.9 nondet()
In the 4th bullet, replace "value set" by "Value Set".
-
6.2.1.1 Sequential FL properties
- Replace the second bullet in the informal semantics by:
- The FL property S holds on a given path iff either there exists a
prefix of the path on which S holds tightly, or the property S! does
not fail on any finite prefix of the given path.
- Replace the Note by:
NOTE-If S contains no contradictions, a simpler description of the
semantics of the property S can be given as follows: The FL property S
holds on a given path iff either there exists a prefix of the path on
which S holds tightly, or every finite prefix of the given path can be
extended to a path on which S holds tightly.
-
6.3.2.1. Sequence declaration
Change "const" to "const numeric" in the first sequence declaration
-
6.3.2.2 Property declaration
Change "const" to "const numeric" in the two properties declarations.
-
Appendix A.4.8
Replace Value_List by Value_Set in the following places:
- the syntax production for built-in function 'nondet' (A.4.8, p127)
- the syntax production for built-in function 'nondet_vector' (A.4.8, p127)
- Appendix B.2 Syntax:
In the note at the top of page 130: Change "efine" to "We define"
- Change "PSL" in PSL_identifier to be in italic font in the following places:
- Page 94, first and second lines of the paragraph "informal semantics"
- A.4.6 page 125 - the rule for Parameter_definition
Last updated on 19 Nov 2007.