[sv-ac] P1800-2009 : Mantis 0002578 comments

Dmitry
The issue is the LRM
16.15.8 Nonvacuous evaluations
d) An evaluation attempt of a property of the form not property_expr is
nonvacuous if, and only if, the underlying evaluation attempt of
property_expr is nonvacuous.

Question, when is it ever vacuous?
 a |-> b --> Vacuous success if a == 0. The "not" will negate it and hence:
not (a |-> b) --> when"a == 0" is a FAILURE

But logically, the intent here is as follows:
not (a |-> b) should mean "never the case that (if a==1, b==1)", and if
a==0, we don't care".  But this is not what "not (a |-> b)" says.  It
says "never the case that (if a==1, b==1)", and if a==0, It's a ERROR".c

Answers to Daniel Mlynek:

>  <1. rule for or operator e)Results should be also vacuous if both prop1
> and prop2 are vacuous.
>
> I'm assuming than if prop1 is non-vacuous pass and prop2 is vacuous pass
> then result is nonvacuous>
>
> Ben: But either one or the other satisfy the requirement.  Doesn't that
> imply both? It's redundant.
>
>
> <4. Operator "not" also introduces ambiguity (for definition see below) -
> what should happen if property under not passes vacuously? We are geting a
> vacuous fail ?
> An evaluation attempt of a property of the form not property_expr is
> nonvacuous if, and only if, the underlying evaluation attempt of
> property_expr is nonvacuous.>
>
> Ben: Agree with the ambiguity.  The way the LRM stands, I don't see how
> the not operator on a property can produce a vacuous result.  In "16.13.16
> Case", LRM brings the concept of true vacuous in "…and the evaluation of
> the case property statement from that start point succeeds and returns true
> (vacuously)." Thus, the not of a property that is vacuous, which is true
> vacuous, must be FALSE.   Consider the property expression:  a |-> b.  If
> "a==0", property expression is vacuous.  But "not(a |-> b)" sates never
> the case that if "a" then "b".  What happens if "a==0"? we should not
> really care, and the not of a vacuous property should  result in a vacuous
> result.
>
> The  statement "An evaluation attempt of a property of the form not
> property_expr is nonvacuous if, and only if, the underlying evaluation
> attempt of property_expr is nonvacuous." Seems to imply that result of a not
> of vacuous property is vacuous.  But vacuous is also considered as "true",
> thus not of true is false.
>

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