RE: [$ieee-1850] Illegal example in LRM: Is it illegal?

Avigail,

I really agree with Tej here. We should not let implementation details
drive the functionality of operators in the language. If the user means

forall j in {0:7}:
     forall k in {0:j}:
         f(j,k)

the verification tool should try to verify this, not complain that it
cannot be handled efficiently (and then error out). In case it can be
handled efficiently[1] by the tool, everything is fine. In case not, the tool
might have to resort to replication. In either case, we should not put
these restrictions on the forall operator.

BTW, it is the same thing with having the forall operator work on any
level, not just the top level of properties. There are quite a few cases
where a property could be expressed very naturally with forall in case you
could use it on any level. In the current language, you have to resort to
_manual_ replication to express the property you want your verification
tool to address for those cases.

Best regards,

--
Johan Alfredsson              Mobile:      +46 706 39 12 58
Product Manager               Office:      +46 31 745 19 00
Safelogic                     Fax:         +46 31 745 19 39
Arvid Hedvalls Backe 4        johan.alfredsson@safelogic.se
411 33 Göteborg, Sweden       www.safelogic.se
[1] In the case above, handling the property with actual replication
     might be the most efficient way, but I guess my message will come
     across anyway.
On Tue, 19 Oct 2004, Avigail Orni wrote:
>
> Hi Tej,
>
>> But there are other cases
>> also apart from this illegal example where it is not possible to
>> implement it in non-replicating way. So why single out this case and
>> make it illegal?
>
> I think we should make sure that all of these cases are clearly disallowed
> in the LRM. If this can be done without ambiguity simply by listing the
> restrictions, then that's great. But I suspect that in some cases an
> example will be necessary in order to prevent any incorrect interpretation.
> Maybe that's why this case was singled out in the previous version.
>
>> I think we should club this issue with Issue #36 raised by Ben Cohen
> I agree!
>
> Avigail
> _______________________________________________________
> Avigail Orni
> Verification and Testing Solutions Group
> IBM Haifa Research Laboratory
> Phone:  972-4-829-6396    email: ornia@il.ibm.com
>
> owner-ieee-1850@eda.org wrote on 18/10/2004 19:35:05:
>
>> Hi Avigail,
>>
>> Thanks for the clarification. I agree that sometimes it is more
>> efficient to implement forall differently. But there are other cases
>> also apart from this illegal example where it is not possible to
>> implement it in non-replicating way. So why single out this case and
>> make it illegal?
>>
>> I think we should club this issue with Issue #36 raised by Ben Cohen
>> since it depends on what we want to write in LRM about non-replicating
>> implementation of forall.
>>
>> Tej
>>
>>
>>> -----Original Message-----
>>> From: Avigail Orni [mailto:ORNIA@il.ibm.com]
>>> Sent: Monday, October 18, 2004 4:28 AM
>>> To: Singh, Tej
>>> Cc: ieee-1850@eda.org; owner-ieee-1850@eda.org
>>> Subject: Re: [$ieee-1850] Illegal example in LRM: Is it illegal?
>>>
>>>
>>> Hi Tej,
>>>
>>> I think that in this case the restriction is correct, but the
>>> text that states that "The parameter defined by a replicator
>>> is considered a static variable" should be changed.
>>>
>>> Your question underlines a general problem that exists in the
>>> "Replicated properties" section. The current text does not
>>> clarify two important
>>> points:
>>>
>>> (1) An implementation of "forall" might not actually
>>> replicate the property. It is sometimes more efficient to
>>> implement "forall" differently, and this should be allowed.
>>>
>>> (2) As a result of the previous point, the replicator
>>> parameter cannot really be considered to be a static
>>> variable. On the other hand, it's not really a dynamic
>>> variable either. I think the text should not try to
>>> categorize the replicator parameter, but should define its
>>> allowed behavior by listing the restrictions. These specify
>>> which behavior must be supported by all implementations, and
>>> which behavior should not be allowed.
>>>
>>> The specific restriction that you mention is important if we
>>> wish to allow non-replicating implementations.
>>>
>>> I hope that the LRM committee will succeed in rewriting this
>>> section so that it more clearly reflects the intent of the
>>> language definition.
>>>
>>> Regards,
>>> Avigail
>>>
>>> _______________________________________________________
>>> Avigail Orni
>>> Verification and Testing Solutions Group IBM Haifa Research Laboratory
>>> Phone:  972-4-829-6396    email: ornia@il.ibm.com
>>>
>>> owner-ieee-1850@eda.org wrote on 14/10/2004 21:03:22:
>>>
>>>> Hi All,
>>>>
>>>> One of the illegal example in 'Sec 6.2.3 Replicated properties' is
>>>>
>>>> forall j in {0:7}:
>>>>     forall k in {0:j}:
>>>>         f(j,k)
>>>>
>>>> I fail to understand why this example is illegal. Probably
>>> because a
>>>> replicator parameter is used in the Value range of the
>>> nested replicator.
>>>> But nowhere does the LRM say that this is illegal. Per LRM
>>>>
>>>> "If a Range is used to specify a Value Range, the Range shall be a
>>>> finite Range, each bound of the Range shall be statically
>>> computable,
>>>> and the left bound of the Range shall be less than or equal to the
>>>> right bound of the Range."
>>>>
>>>> A replicator parameter is static variable. Thus  {0:j}
>>> satisfies the
>>>> restrictions on value range.
>>>>
>>>> Should this example be removed from the LRM?
>>>>
>>>> Regards
>>>> Tej
>>>>
>>>
>>>
>>
>
>