[sv-ac] RE: formal semantics is ready for review (resent to the whole forum)

Hi Doron,

Here are my comments:

* The semantics of the recursive property instantiation requires a
further elaboration. There is a cryptic statement in the current version
of LRM: 

"Once the semantics of the recursive property instances is understood,
the placeholder functions are treated as properties with this
semantics."

You probably need to expand the abstract syntax to include a recursion
operator.

* In the sentence: "The semantics of recursive properties is defined in
clause {\bf F.5} in terms of an infinite sequence of nonrecursive
properties, possibly with instances of properties and sequences."

the term "sequence" is overloaded: the first time it has its common
meaning, while the second time it has its SV meaning.

* $var function is used before being defined: a forward reference is
necessary.

* The following sentence is not clear: "The return value of a
nonrecursive property associated with the recursive property is the
return value of the sub {\tt property\_expr} resulted from flattening an
instance of the
nonrecursive property in the place of the recursive one."

What is a return value of a property?

* The formal definition of $var() function is missing

* The following essentially means that each sequence and property
defines its own scope for local variables. "For every local variable
declared in {\tt P'}, make its name unique with respect to the names of
the local variables declared in the property\_expr of the assertion."

It would be more intuitive if it is explicitly stated. It is also
important to state it in Clause 16. 

Thanks,
Dmitry

-----Original Message-----
From: Doron Bustan [mailto:dbustan@freescale.com] 
Sent: Thursday, May 10, 2007 10:33 PM
To: John Havlicek; Korchemny, Dmitry
Cc: Lisa Piper; Singh, Tej; Bassam Tabbara
Subject: formal semantics is ready for review

it is uploaded at mantis 1549 and attached.

Doron

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