Subject: Re: LRM examples for replicated properties
From: Cindy Eisner (EISNER@il.ibm.com)
Date: Tue Sep 02 2003 - 04:05:46 PDT
sunny,
unless i've missed something (i've been on vacation for the past month), i
think that no one has answered this yet either.
regarding your issue #1 ("The LRM's examples appear to suggest that
parameterized named properties can specify array/vector typed formals"):
allowing this was the intention, as shown by the examples and by the formal
semantics of forall in section b.3.3. thus, i would consider the lack of
grammar support for this an oversight, which needs to be fixed.
regarding your issue #2 (status of the name defined by a replicator): the
original intention is that the name defined by a replicator is a special
kind of variable - one that is known to keep its value for the duration of
a particular trace. thus it is half-way between a variable and a constant,
in some sense. one way to implement such a thing is to simply replicate
the formula the requisite number of times, thus pushing the replicator over
the border into constant land. this is probably the source of the wording
"statically evaluable integer expression". however, implementing foralls
in such a way can be very inefficient. other implementations would
preserve more of the "variable-ness" of the replicator. if i recall
correctly, the wording "The Name defined by a replicator represents a
non-static variable" was an attempt to address the scoping issues - if you
have two "forall i" statements, the i's are distinct. so - that was the
intention. i agree that the wording of the lrm needs work.
regards,
cindy.
--------------------------------------------------------------------
Cindy Eisner
Formal Methods Group
IBM Haifa Research Laboratory
Haifa 31905, Israel
Tel: +972-4-8296-266
Fax: +972-4-8296-114
e-mail: eisner@il.ibm.com
"Yum, Sunny" <Sunny_Yum@mentorg.com>@eda.org on 19/08/2003 23:15:37
Sent by: owner-vfv@eda.org
To: "'vfv@eda.org'" <vfv@eda.org>
cc:
Subject: LRM examples for replicated properties
I have come up with two issues that regard the examples for replicated
properties provided by the PSL LRM (v1.01) in section 6.2.3.
Issue #1: The LRM's examples appear to suggest that parameterized named
properties can specify array/vector typed formals. To my knowledge, the
PSL
LRM does not specify support for parameterized named properties with
array/vector typed formals.
Example "forall i[0:1] in boolean : f(i)" suggests that the parameterized
named property "f" has a single formal parameter that is a two-element
array/vector of type boolean.
Example "forall i[0:2] in {4,5} : f(i)" suggests that the parameterized
named property "f" has a single formal parameter that is a three-element
array/vector of type integer.
Issue #2: Despite the fact that the LRM states that "The Name defined by a
replicator represents a non-static variable", the following examples
illustrate the use of a replicator name (of integer type) that is being
used
to instantiate a parameterized named property, in contradiction to the
statement in section 6.2.4.2 (Property Instantiation) that states "For a
const parameter, the actual parameter shall be a statically evaluable
integer expression".
Example "forall I in {j:k} : f(i)" (assuming that j and k are integer
literals) suggests that the replicator name "I" is being used as an actual
parameter (const) to instantiate the parameterized named property "f".
Example "forall I in {j,l} : f(i)" (assuming that j and l are integer
literals) suggests that the replicator name "I" is being used as an actual
parameter (const) to instantiate the parameterized named property "f".
Can anyone shed some light on either of these issues for me? Thanks.
-Sunny
This archive was generated by hypermail 2b28 : Tue Sep 02 2003 - 03:59:50 PDT