Subject: [sv-ac] errata for Annex H
From: John Havlicek (john.havlicek@motorola.com)
Date: Thu Jan 22 2004 - 15:15:53 PST
SVA 3.1A DRAFT 3 ERRATA, JH GROUP 2
================================================================================
Errata in Appendix H
================================================================================
ERRATRUM JH3: pp. 484-485, H.2.1. There is a font inconsistency
in the abstract grammars. In the grammars for unclocked sequences,
clocked sequences, and assertions, non-terminals are set in
roman italic, while in the grammars for unclocked properties and
clocked properties, non-terminals are set in courier italic. The
font should be roman italic.
ERRATRUM JH4: pp. 484-485, H.2.1. There is a spacing inconsistency
in the abstract grammars. In the grammars for unclocked sequences
and clocked sequences, space is provided between tokens on the right-hand
sides of productions, while in the grammars for unclocked properties and
clocked properties such space is not provided. One or the other sets
of grammars should be changed. This is an aesthetic issue.
ERRATUM JH5: p. 484, H.2.1, bottom of the page. There seems to
be space missing before the last sentence on the page. Change
... non-degenerate unclocked sequence.See H.3.2 ...
to
... non-degenerate unclocked sequence. See H.3.2 ...
ERRATUM JH6: p. 485, H.2.1, the two sentences following the grammar
for clocked properties. There seems to be space missing before the
last sentence on the page. Change
... non-degenerate clocked sequence.See H.3.2 ...
to
... non-degenerate clocked sequence. See H.3.2 ...
ERRATUM JH7: p. 485, H.2.2. Delete the sentence
The following auxiliary notions will be used in defining the semantics.
Rationale: All of these notions were deleted.
ERRATUM JH8: p. 485, H.2.2. Delete the clause
N, N_1, N_2 denote negation specifiers;
Rationale: All references to negation specifiers have been deleted.
ERRATUM JH9: p. 485, H.2.2. Change
P denotes an unclocked property
to
P, P_1, P_2 denote unclocked properties.
Rationale: H.2.3.5 refers to P_1 and P_2.
ERRATUM JH10: p. 487, H.3.1. Third bullet. Change
@(c) ( P ) |---> @(c) P .
to
@(c) ( P ) |---> ( @(c) P ) .
Rationale: The parentheses should not be lost. I think they were in
the change request.
ERRATUM JH11: p. 487, H.3.1, last two bullets. The fonts used
for the clock rewrite rules for "and" and "or" do not match the
style of the other bullets. The terminals "@", "(", ")" should be
set in courier and the keywords "and" and "or" should be set in
courier bold.
ERRATUM JH12: H.3.2, p. 488. The two dashed sub-bullet items
under the the seventh bullet (first_match) need to be indented.
ERRATUM JH13: p. 488, H.3.3.1. In the first bullet under "Neutral
satisfaction of assertions", change
w^i |= b
to
\overline{w}^i |= b
ERRATUM JH14: p. 488, H.3.3.1. In the third bullet under "Neutral
satisfaction of assertions", delete "then". Also delete the parentheses
around the clause after "iff".
ERRATUM JH15: pp. 488-489, H.3.3.1. In the third bullet under
"Neutral satisfaction of properties", change
\vee^\omega
to
\top^\omega
(\top is the sans-serif symbol that looks like "T". You might be using
an Arial "T" for it.)
ERRATUM JH16: p. 489, H.3.3.1. Change the remark at the end of this
section from
Remark: It can be proved ...
to
Remark: Since w is non-empty, it can be proved ...
Rationale: People have been confused about this because they forget
that the assumption w non-empty applies throughout H.3.3.1.
ERRATUM JH17: p. 489, H.3.3.2. In the first bullet, change the italic
"T" to "\top".
ERRATUM JH18: p. 489, H.3.3.2. Change
A tool checking for satisfaction of A by the finite word w should return
* "true" if w |=^+ A.
* "false" if w |/=^- A.
* "unknown" otherwise.
to
A tool checking for satisfaction of A by the finite word w should return
* "holds strongly" if w |=^+ A.
* "fails" if w |/=^- A.
* "pending" or "holds weakly" otherwise.
Rationale: This wording is to achieve alignment with PSL.
ERRATUM JH19: p. 489, H.3.4, second paragraph, second sentence. Change
sampled in the sequence
to
sampled (i.e., assigned) in the sequence
Rationale: Some people have (reasonably) expressed confusion that
the local variable is being said to be "sampled" rather than
"assigned".
ERRATUM JH20: p. 491, H.3.5, first full sentence. It is difficult
to see visually the beginning of the definition of tight satisfaction
because this sends ends with displayed statements that are not
centered. I think the display formatting should be changed to
paragraph formatting: change
It can be proved that this definition guarantees that
w,L_0,L_1 |== R implies dom(L_1) = flow(dom(L_0),R).
to
It can be proved that this definition guarantees that w,L_0,L_1 |== R
implies dom(L_1) = flow(dom(L_0),R).
ERRATUM JH21: p. 491, H.3.5, first bullet on the page. Change the
display formatting of
L_1 = {(v,e[L_0,w^0])} \union L_0|_D
to paragraph formatting.
ERRATUM JH22: p. 491, H.3.5, first bullet on the page. Restore the
definition
and D = dom(L_0) - {v}
that is struck out.
Rationale: We need to keep this definition since we use "D" two lines above.
ERRATUM JH23: p. 491, H.3.5, sixth bullet on the page. The dashed
sub-bullet items need to be indented.
ERRATUM JH24: p. 491, H.3.5, eighth bullet on the page. The dashed
sub-bullet items need to be indented.
ERRATUM JH25: p. 491, H.3.6.1, second paragraph. Change
rules defining neutral satisfaction of an assertion satisfaction are
to
rules defining neutral satisfaction of an assertion are
ERRATUM JH26: p. 492, H.4.1. There are font errors in the second
and fourth lines of this section. In the second line, "V" should be
italic. In the fourth line, "D" should be italic (2 instances) and
"V" should be italic (2 instances).
ERRATUM JH27: p. 493, H.5, second paragraph. The keyword phrases
"not" and "disable iff" appear in roman. In Appendix H, keyword
phrases should be in courier bold.
ERRATUM JH28: p. 493, H.5, third paragraph, first sentence. "depend"
should be italic as this word is being given a technical definition.
ERRATUM JH29: p. 493, H.5, third paragrph. Font errors: "n" should
be italic (2 instances); "i" should be italic (2 instances).
ERRATUM JH30: p. 493, H.5, fourth paragraph, first sentence.
"dependency digraph" should be italic as this phrase is being given
a technical definition.
ERRATUM JH31: p. 493, H.5, example in the middle of the fourth
paragraph. "q" should be roman italic; "r" should be roman italic
(2 instances).
ERRATUM JH32: p. 493, H.5, fifth paragraph (the sentence defining
"recursive"). "p" should be roman italic. "recursive" should be
italic as this word is being given a technical definition.
ERRATUM JH33: p. 493, H.5, last line. Font error: "L" should
be italic.
This archive was generated by hypermail 2b28 : Thu Jan 22 2004 - 15:25:52 PST