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

We all agree that there is an inconsistency in the text. Some of us think
it should be solved by not calling the replication parameter a "static
variable". Others think it should be solved by removing the restriction.

Since there is a lack of agreement about the essential semantics that
"forall" should have, I believe this is no longer a straightforward subject
for the LRM subcommittee, and should be discussed in the Extensions
subcommittee. I would give it high priority.

_______________________________________________________
Avigail Orni
Verification and Testing Solutions Group
IBM Haifa Research Laboratory
Phone: 972-4-829-6396 email: ornia@il.ibm.com

Johan Alfredsson <johan.alfredsson@safelogic.se> wrote on 19/10/2004
14:58:33:

>
> 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
> >>>>
> >>>
> >>>
> >>
> >
> >
Received on Tue Oct 19 07:28:03 2004