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

Hi Dmitry:

Thanks for looking at this.  I would like to have some discussion 
of these points before changing the proposal for Annex F.  Please
see my responses and questions below.

J.H.

> Hi John,
> 
> Here are my comments:
> 
> Page 6.
> 
> * I think that the terms "semantic leading edge" and "inherited" clock
> require a formal definition

Yes, I agree that these should be defined.  I believe that the
definitions in 16.15.1 are adequate.  Please check and see if you
agree.  We could add a reference to 16.15.1 to help the reader 
find them.

> 
> * The definition push(E; r) =3D \kappa(r) (1, E) ##0 ( r ) does not say
> anything about the case when r matches an empty word

True.  If the recursive descent of push reaches a point where
push(E,r) is evaluated, then r must be a sequence property.

In 16.12, item a) on p. 341, it says

   A sequence that admits an empty match is not allowed as a property.

Therefore, I don't think push(E,r) has to worry about whether r admits
empty match.  The compiler should reject r in this case, and push
would not need to be evaluated.

If in the future we decide to lift the restriction from 16.12, then we
will have to decide how the property satisfaction relation should be
defined for a sequence property admitting empty match and how push should
be changed.

Do you agree?  If so, what changes would you like to see now in the
proposal for Annex F?

> 
> * The definition of push(...|=3D>...) does say about the case when r
> matches the empty word, but we don't have a definition of the empty word
> match before the rewriting

Hmm.  This also is true.  One solution is that we make a special
definition of admitting empty match.  Something like

  \emptyword |=/= b
  \emptyword |=/= (1, list_of_sequence_match_items)
  \emptyword |== ( r ) iff  \emptyword |== r
  \emptyword |== r ##1 r'  iff  \emptyword |== r and \emptyword |== r'
  \emptyword |=/= r ##0 r'
  \emptyword |== r or r'  iff  \emptyword |== r or \emptyword |== r'
  \emptyword |== r intersect r'  iff  \emptyword |== r and \emptyword |== r'
  \emptyword |== first_match(r)  iff  \emptyword |== r
  \emptyword |== r[*0]
  \emptyword |== r[*1:$]  iff  \emptyword |== r
  \emptyword |== @(c) r  iff  \emptyword |== r
  
    
Of course, then this raises the question of whether our other definition
of |== is consistent with this one for \emptyword -- presumably that is 
straightforward to check.

Can you think of a better way to address this problem?


> X-ExtLoop1: 1
> X-IronPort-AV: E=Sophos;i="4.16,581,1175497200"; 
>    d="scan'208";a="272549155"
> X-MimeOLE: Produced By Microsoft Exchange V6.5
> Content-class: urn:content-classes:message
> Date: Wed, 25 Jul 2007 17:55:35 +0300
> X-MS-Has-Attach: 
> X-MS-TNEF-Correlator: 
> Thread-Topic: [sv-ac] 1668-formal-semantics.pdf
> Thread-Index: AcfEg8+bycaaDwYIQaKUiEfKs/VB6AKO/B/Q
> From: "Korchemny, Dmitry" <dmitry.korchemny@intel.com>
> X-OriginalArrivalTime: 25 Jul 2007 14:55:39.0241 (UTC) FILETIME=[DD742D90:01C7CECB]
> 
> Hi John,
> 
> Here are my comments:
> 
> Page 6.
> 
> * I think that the terms "semantic leading edge" and "inherited" clock
> require a formal definition
> 
> * The definition push(E; r) =3D \kappa(r) (1, E) ##0 ( r ) does not say
> anything about the case when r matches an empty word
> 
> * The definition of push(...|=3D>...) does say about the case when r
> matches the empty word, but we don't have a definition of the empty word
> match before the rewriting
> 
> Thanks,
> Dmitry
> 
> -----Original Message-----
> From: owner-sv-ac@server.eda.org [mailto:owner-sv-ac@server.eda.org] On
> Behalf Of John Havlicek
> Sent: Thursday, July 12, 2007 3:52 PM
> To: sv-ac@server.eda-stds.org
> Subject: [sv-ac] 1668-formal-semantics.pdf
> 
> Hi All:
> 
> I have uploaded the 1668-formal-semantics.pdf to Mantis
> and attached it here. =20
> 
> J.H.
> 
> --=20
> This message has been scanned for viruses and
> dangerous content by MailScanner, and is
> believed to be clean.

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