Re: [sv-ac] 1668-formal-semantics.pdf

Hi Doron:

Thanks for looking at this.

> 1. I don't understand the bullet at F.2.3.5
> 
>     Should it be:
> 
>     For i<k-1
> 
>     ( ti vi [=3D ei];...;tk vk [=3D ek];X) \equiv
>     ( ti vi [=3D ei]; ti+1 vi+1 [=3D ei+1];...;tk vk [=3D ek];X)
>     ?

I don't think what you have shown here adds any information.

Here is what I was trying to do with this bullet.

The original syntax allows attaching one local variable declaration
with optional assignment to an expression X via


   (t v [= e] ; X)

This bullet is trying to say how to attach a list of semicolon-
separated local variable declarations, each with optional assignment,
by reducing inductively to the original case in which only one
declaration is attached at a time.

The bullet is trying to say

   (t1 v1 [= e1]; t2 v2 [= e2]; X) 

   \equiv 

   (t1 v1 [= e1]; (t2 v2 [= e2]; X))

and 

   (t1 v1 [= e1]; t2 v2 [= e2]; t3 v3 [= e3]; X) 

   \equiv 

   (t1 v1 [= e1]; (t2 v2 [= e2]; t3 v3 [= e3]; X))

   \equiv

   (t1 v1 [= e1]; (t2 v2 [= e2]; (t3 v3 [= e3]; X)))

etc.

> 2. I am not sure it belongs in 1668, but we need to add the LTL
> operators to     the push definition.=20

Someone will have to do it.  I haven't thought yet about what 
push should look like for LTL forms.  Have you?  My guess is 
that it will not be hard to figure this out.

J.H.

> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.19,197,1183359600"; 
>    d="scan'208";a="272097528"
> X-MIMEOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Mon, 30 Jul 2007 08:29:15 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1668-formal-semantics.pdf
> Thread-Index: AcfO2/phtONqNktXQpGbnWKvhBkFHwDjYhNQ
> From: "Bustan, Doron" <doron.bustan@intel.com>
> Cc: <sv-ac@eda-stds.org>
> X-OriginalArrivalTime: 30 Jul 2007 05:29:16.0139 (UTC) FILETIME=[920313B0:01C7D26A]
> 
> Hi John,=20
> 
> In general it looks good!
> Here are my comments:
> 
> 1. I don't understand the bullet at F.2.3.5
> 
>     Should it be:
> 
>     For i<k-1
> 
>     ( ti vi [=3D ei];...;tk vk [=3D ek];X) \equiv
>     ( ti vi [=3D ei]; ti+1 vi+1 [=3D ei+1];...;tk vk [=3D ek];X)
>     ?
> 
> 2. I am not sure it belongs in 1668, but we need to add the LTL
> operators to     the push definition.=20
> 
> Doron
> 

-- 
This message has been scanned for viruses and
dangerous content by MailScanner, and is
believed to be clean.