[sv-champions] Re: [sv-sc] some comments on 1900, part 2

Hi Mike:

My only concern of substance is whether "const" is clear in "const or
automatic value".  Is it better to use the phrase "const cast"?
Aligning to a turn of phrase appearing in 17.3 may help.

As a bit of wordsmithing, you might consider changing 

  "Any of these assume statements that <do something bad> are excluded
  from the assume set."

to

  "Any of these assume statements that <does something bad> is excluded
  from the assume set."

J.H.

> Date: Wed, 13 Aug 2008 11:19:16 -0700
> From: Michael Burns <michael.burns@freescale.com>
> CC: shalom.bresticker@intel.com, sv-champions@eda.org, sv-sc@eda.org
> X-OriginalArrivalTime: 13 Aug 2008 18:19:19.0556 (UTC) FILETIME=[1A5E0440:01C8FD71]
> 
> 
> Hi John, Shalom, and everyone else,
> 
> Here's my crack at recasting that paragraph - what do you think?
> 
> "The assume set of a checker instance is formed from the checker assume statements and child checker assume statements. Any of these assume statements that reference a formal whose actual expression contains any subexpression that is a const or automatic value (see 17.3) are excluded from the assume set. This restriction allows one copy of the assume set to exist in every time step as described in 17.3.1. Among the remaining assume statements, those that reference active free variables of the checker are included in the assume set..."
> 
> I'm ready to post my edited doc - if anyone doesn't like this phrasing, please let me know.
> 
> Thanks,
> --Mike
> 
> John Havlicek wrote:
> > Hi Mike:
> > 
> >> I mean "const" in the same sense as is described in 16.15.5.1 in Mantis 2398 - an actual expression involving terms that are either explicitly const-cast or implicitly treated as as const-cast because they are automatics.
> >>
> > 
> > I read that meaning into your use of the phrase "constant actuals (see
> > 17.3)".
> > 
> > However, I think Shalom has a point that getting this meaning is
> > asking a lot of a reader who hasn't participated in or had visibility
> > into what went on in SV-SC.
> > 
> > Can you massage the phrase
> > 
> > (*) an actual expression involving terms that are either explicitly
> >     const-cast or implicitly treated as as const-cast because they are
> >     automatics
> > 
> > into something that can be used instead of "constant actual".  Maybe
> > you can find a short phrase that doesn't already have a defined
> > meaning and define it to mean (*) and then use the short phrase.
> > 
> > J.H.
> > 
> >> Date: Wed, 13 Aug 2008 07:59:26 -0700
> >> From: Michael Burns <michael.burns@freescale.com>
> >> CC: john.havlicek@freescale.com, sv-champions@eda.org, sv-sc@eda.org
> >> X-OriginalArrivalTime: 13 Aug 2008 14:59:30.0252 (UTC) FILETIME=[302F68C0:01C8FD55]
> >>
> >>
> >> Shalom,
> >>
> >> Bresticker, Shalom wrote:
> >>> Mike, thanks. 
> >>>
> >>>>> Do you mean "constant actuals" or "const actuals"? If an 
> >>>> actual is a 
> >>>>> real constant, such as a number or a parameter, is that 
> >>>> included? What 
> >>>>> about a const NON-free variable? If "constant" is used too loosely 
> >>>>> here, it may be in other places as well, and this should be checked.
> >>>> No, I mean const actuals. That I must change - I used 
> >>>> "constant" in one part, which is wrong. It doesn't matter 
> >>>> whether the const actual is a free variable or not.
> >>> So I am now unclear again. When you write here "const actual", what do
> >>> you mean? Please define precisely.
> >> I mean "const" in the same sense as is described in 16.15.5.1 in Mantis 2398 - an actual expression involving terms that are either explicitly const-cast or implicitly treated as as const-cast because they are automatics.
> >>
> >> --Mike
> >>
> >>> Thanks,
> >>> Shalom
> >>> ---------------------------------------------------------------------
> >>> Intel Israel (74) Limited
> >>>
> >>> This e-mail and any attachments may contain confidential material for
> >>> the sole use of the intended recipient(s). Any review or distribution
> >>> by others is strictly prohibited. If you are not the intended
> >>> recipient, please contact the sender and delete all copies.
> >>>

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