Proposed LRM changes for "forall" issues

Hi all,
Here are the proposed LRM changes for the "forall" issues discussed in
recent extensions subcommittee meetings.

The changes are grouped into two categories:
(1) Changes for clarifying the meaning of forall
(2) Changes for removing the restriction that forall may only be used at
the top level of properties

(1) Changes for clarifying the meaning of forall
------------------------------------------------

(I) Section 6.2.3 Replicated properties

(I.a) Add the following note after Box 78 (page 79)
"Note: the term "/replicated/ /property/" is used figuratively. It does not
imply that replication actually takes place. Whether or not any part of the
property is replicated depends on the implementation".

(I.b) Change the paragraph on page 79, lines 53-55, to the following:
"1) If the parameter is not an array, then the property is equivalent to a
property obtained by the following steps:
(i) replicating the parameterized property for each value in the set of
values, with that value substituted for the parameter (so that the total
number of replications is equal to the size of the set of values)
(ii) logically "anding" all of the replications."

(I.c) Change the paragraph on page 80, lines 1-4, to the following:
"2) If the parameter is an array of size N, then the property is equivalent
to a property obtained by the following steps:
(i) replicating the parameterized property for each possible combination of
N (not necessarily distinct) values from the set of values, with those
values substituted for the N elements of the array parameter (if the set of
values has size K, then the total number of replications is equal to K^N)
(ii) logically "anding" all of the replications."

(I.d) Add the following paragraph after the preceding paragraph (page 80,
line 5):
"Note that in both cases the meaning of a replicated property is
/equivalent/ to the replication process. This does not imply that any
replication must actually take place."

(I.e) Change the note on page 80, lines 37-38, to the following:
"Note— The parameter defined by a replicator is considered to be statically
computable..."

(I.f) Replace the Informal Semantics section (starting on page 80, line 40)
with the following:

—A forall i in boolean: f(i) property is equivalent to:
f(true) && f(false)

—A forall i in {j:k} : f(i) property is equivalent to:
f(j) && f(j+1) && f(j+2) && ... && f(k)

—A forall i in {j,l} : f(i) property is equivalent to:
f(j) && f(l)

—A forall i[0:1] in boolean : f(i) property is equivalent to:
f({false,false}) && f({false,true}) && f({true,false}) && f({true,true})

—A forall i[0:2] in {4,5} : f(i) property is equivalent to:
f({4,4,4}) && f({4,4,5}) && f({4,5,4}) && f({4,5,5})
      && f({5,4,4}) && f({5,4,5}) && f({5,5,4}) && f({5,5,5})

(2) Changes for removing the top-level requirement
--------------------------------------------------

(I) Section 6.2.3. Replicated properties

(I.a) Remove the following paragraph (page 80 lines 33-35)
"A replicator may appear in the declaration of a named property, provided
that instantiations of the named property
do not violate the above restriction. This means that the replicator must
be at the top level of the named property
declaration, and the named property's instantiations must not appear inside
non-replicated properties."

(I.b) Remove the titles "Legal:" and "Illegal:" from the examples (page 81
lines 31, 44).
All of the examples are now legal.

(I.c) Add parentheses around the operand of forall in the third example
(for educational purposes, although they are not strictly necessary):
"always (request ->
forall i in boolean: (next_e[1:10](response[i])))"

(I.d) Add the following note (perhaps under the "examples" heading, before
the examples themselves):
"Note: due to the low precedence of the forall operator, it is often
necessary to apply parentheses to the operand of forall, especially when
the forall operator is nested inside other operators."

(I.e) Change the grammar in Box 78 (page 79) according to the syntax
changes below.

(II) Appendix A Syntax rule summary
In the current grammar, the "replication" operator is applied to properties
in general, only at the top level. The proposed change is to apply it to FL
properties at any level, but to apply it to OBE properties only at the top
level (in order to maintain the structure of the OBE, with its limited set
of operators). The detailed changes are listed below.

(II.a) Section A.4.4 PSL properties

Current grammar:
FL_Property ::=
      Boolean (see A.4.7)
      | ( FL_Property )
      | Sequence [ ! ]
      | property_Name [ ( Actual_Parameter_List ) ]
      | FL_Property @ Clock_Expression
      | FL_Property abort Boolean
      | Replicator FL_Property <---- ADD THIS LINE
......

(III) Section 4.2.3 Operators

(III.a) Add the forall operator to "Table 2 -- FL operator precedence and
associativity", page 14.
The forall operator should appear in the last line of the table (lowest
precedence).
It can be given right associativity (this has no meaning since it is not an
infix operator).

(III.b) Add section 4.2.4 "Forall operator" (on page 17, before the
"Macros" section)
"For any flavor of PSL, the operator with the lowest precedence is the
forall operator, which is
used as shorthand for an "and" operation performed on a set of properties.
In FL properties, the forall operator may be applied to any sub-property.
In OBE properties, the forall operator may only be applied at the top level
of the property.

The forall operator is right-associative."

_______________________________________________________
Avigail Orni
Verification and Testing Solutions Group
IBM Haifa Research Laboratory
Phone: 972-4-829-6396 email: ornia@il.ibm.com
Received on Tue Dec 7 03:52:39 2004