Re: [sv-ac] 1420

Hi Manisha:

> Note that argument order has changed in this case. Now it can be
> interpretted in two ways:
> 1. After each recursion, a and b get switched.
> 2. After first recursion, a and b get switched but after that they
> remain the same.

I think we need to use interpretation 1 in order to be consistent
with the way the semantics of recursive properties is described.
(This got lost from Annex E, but it will be put back.)

I think 

   property P(a, b)
     (a ##1 b) and (1 |=> P(b, a));
   endproperty 

should be equivalent to

   property P(a, b)
     (a ##1 b) and (1 |=> Q(a, b));
   endproperty 


   property Q(a, b)
     (b ##1 a) and (1 |=> P(a, b));
   endproperty 

Why do you see switching the argument order as problematic?

J.H.


> X-Authentication-Warning: server.eda-stds.org: majordom set sender to owner-sv-ac@eda.org using -f
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Mon, 21 Aug 2006 15:18:30 -0700
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1420
> Thread-Index: AcbFbf6WzxapRvBAQ7e4J/WQ3/NOwgAAI/xA
> From: "Kulshrestha, Manisha" <Manisha_Kulshrestha@mentor.com>
> X-OriginalArrivalTime: 21 Aug 2006 22:18:31.0249 (UTC) FILETIME=[BBFB5410:01C6C56F]
> X-Virus-Status: Clean
> X-MIME-Autoconverted: from quoted-printable to 8bit by server.eda-stds.org id k7LMIXDu017209
> Sender: owner-sv-ac@eda.org
> 
> Hi Doron,
> 
> This proposal looks good. One thing which is still an issue is what
> happens when all the arguments are same as formal arguments but the
> order has changed. Is that legal ? If yes, how do we interpret it. Here
> is an example:
> 
> property P(a, b)
> 
> (a ##1 b) and (1 |=> P(b, a));
> 
> endproperty 
> 
> Note that argument order has changed in this case. Now it can be
> interpretted in two ways:
> 1. After each recursion, a and b get switched.
> 2. After first recursion, a and b get switched but after that they
> remain the same.
> 
> I would prefer if we make it illegal to switch the formal argument order
> also.
> 
> Thanks.
> Manisha
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of Doron Bustan
> Sent: Monday, August 21, 2006 3:05 PM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] 1420
> 
> All,
> 
> we modified the 1420 proposal to deal with the example presented at
> 17.11.4
> 
> I upload it to mantis and also attached it.
> 
> Doron
>