Proposal for Parameterized And/Or operators

Erich, All,

Below is a proposal for adding parameterized AND/OR operators for
formula and SEREs. The proposal adds the parameters types as
allowed for forall in the current version LRM v1.1. Any extensions
decided for forall can be applied to the parameterized and/or
operators as well.

  The idea is to first define what is a the set obtained by
  parameterizing a property (or a sequence) and then define what
  it means to perform an and/or operator on a (parameterized) set.

  For example, first we define that for a SERE A, and an identifier
  i, the expression [i in {6..8} ] A(i) is equivalent to the set
  S containing the 3 elements: A(6), A(7) and A(8).
  Then we define that && S is equivalent to A(6) && A(7) && A(8).

  The required changes are elaborated below.

Best regards,
Dana.

1. Changes in the BNF (Appendix A):

 The following productions should be added:

 Parameter_definition ::= [ PSL_Identifier [ Index_Range ] in Value_Set ]
 Parameterized_SERE_Set ::= Parameter_definition Compound_SERE
 Parameterized_ FL_Property _Set ::= Parameter_definition FL_Poperty

 Compound_SERE ::=
 | & Parameterized_SERE_Set
 | && Parameterized_SERE_Set
 | | Parameterized_SERE_Set

 FL_Property ::=
 | AND_OP Parameterized_ FL_Property _Set
 | OR_OP Parameterized_ FL_Property _Set

2. Changes in formal definition (Appendix B):

Addition of the appropriate syntactic sugaring to section B.3.1
(Additional SERE Operators) and to section B.3.2 (Additional SERE
Operators) as indicated in RED in the attached pdf.

3. Changes in the body of the LRM:

I. Two sections should be added:
   a. A section describing parameterized SEREs should be added between
      section 6.1.1.2 to 6.1.1.2.1.
   b. A section describing parameterized properties should be added
      between section 6.2.1.7 to 6.2.1.7.1
   Below is a section describing parameterized SEREs. A section describing
   parameterized properties can be defined similarly (by replacing
   "Compound SERE" with "FL Property").

II. The following sections should be changed to include application
   of the respective operator to a (parameterized) set.
   
   a. Section 6.1.1.2.1 SERE or (|)
   b. Section 6.1.1.2.2 SERE non-length-matching and (&)
   c. Section 6.1.1.2.3 SERE length-matching and (&&)
   d. Section 6.2.1.7.3 Logical and
   e. Section 6.2.1.7.4 Logical or

   Below are sections for SERE or (|) and Logical and. The others
   sections can be defined similarly.

-------------------------------------

Parameterized SEREs

Introduction:
The parameterizing operators, shown in Box xxx,
constructs a set of Compound SEREs, each element in the set is
obtained by instantiating a different possible value of the given
parameter in the given compound SERE.

Box:
 Parameterized_SERE_Set ::= Parameter_definition Compound_SERE
 Parameter_definition ::= [ PSL_Identifier [ Index_Range ] in Value_Set]

Text following the box:
The operands of the parameterizing
operator are a parameter definition and a parameterized Compound
SERE. The PSL Identifier in the parameter definition is the name
of the parameter in the Compound SERE. This parameter can be an
array. The Value Set defines the set of values the parameter can
obtain.
    1.
    If the parameter is not an array, and the set of
    values has size K then the obtained set is of size K. Each element
    in the set is obtained by substituting the parameter with one of
    the possible values in the set of values.
    2.
    If the parameter is an array of size N, and the set of values has size
    K then the obtained set is of size K^N. Each element in the set is
    obtained by substituting each element in the array with one of the
    possible values in the set of values.

The set of values can be specified in three different ways
 - The keyword boolean specifies the set of values {True, False}.
 - A Value Range specifies the set of all values within the given range.
 - The comma (,) between Value Ranges indicates the union of the obtained
 sets.

Restrictions:
*** Same as in the replicated properties section (6.2.3) ***
....

Informal semantics:

For Compound SERE A

- [i in boolean] A(i) is equivalent to the set containing the two
elements A(false) and A(true)

- [i in {j:k}] A(i) is equivalent to the set containing the
k-j+1 elements: A(j), A(j+1), , A(k)

- [i in {j,l,k}] A(i) is equivalent to the set containing the 3
elements: A(j), A(l) and A(k)

- [i[0:1] in boolean] A(i) is equivalent to the set containing
the 4 elements: ({false,false}), A({false,true}), A({true,false})
and A({true,true})

- [i[0:2] in [c,d]] A(i) is equivalent to the set containing the
8 elements: A({c,c,c}), A({c,c,d}), A({c,d,c}), A({c,d,d}),
A({d,c,c}), A({d,c,d}), A({d,d,c})and A({d,d,d})

-------------------------------------

6.1.1.2.1 SERE or (|)

Introduction:
The SERE or operator (|), shown in Box 28,
constructs a Compound SERE in which one of several alternative
Compound SEREs hold at the current cycle.

Box:
  Compound_SERE ::= Compound_SERE | Compound_SERE
  Compound_SERE ::= | Parameterized_SERE_Set

Text following the box: The operands of |are either two Compound
SEREs or a set of compound SEREs given by a Parameterized_SERE.

Restrictions:
If the operand of | is a parameterized SERE then the
set it defines should be non-empty.

Informal semantics:

For Compound SEREs A and B: A|B holds tightly on a path iff at
least one of A or B holds tightly on the path.

For a Parameterized SEREs Set S: | S holds tightly on a path iff
at least one of the compound SEREs A in S holds tightly on the
path.

-------------------------------------

6.2.1.7.3 Logical and

Introduction: The logical and operator, shown in Box 60, is used
to specify logical and.

Box:
 FL_Property ::= FL_Property AND_OP FL_Property
 FL_Property ::= AND_OP Parameterized_FL_Property_Set

Text following the box: The operands of the logical and operator
are either two FL Properties or a set of FL Properties given by a
Parameterized_ FL_Property _Set.

Restrictions:

If the operand of the logical and is a parameterized property then
the set it defines should be non-empty.

Within the simple subset (see section 4.4.4), if the logical and
has two operands then the left operand of a logical and is
restricted to be a Boolean expression, otherwise all the elements
in the set defined by the parameterized FL property but one are
restricted to be Boolean expressions.

Informal semantics:

A logical and property holds in a given cycle of a given path iff
the FL Properties that are the operands all hold at the given
cycle. That is,

For FL Properties f and g: F AND_OP g holds on a path iff both A
and B holds on the path.

For a Parameterized FL Property Set S: AND_OP S holds on a path
iff all the FL Properties defined by S holds on the path.