Re: [sv-ac] vacuity

All:

Note that "\non" is a relation that defines when an evaluation
is non-vacuous.  "w,L \non P" does not imply "w,L |= P", so that 
"\non" does not say anything about whether the evaluation results
in success or failure.

The definition of "pass non-vacuously" would then be "w,L |= P" 
and "w,L \non P".

Regarding "b" in "disable iff (b) P", it does not affect "\non".

Also, note that if we had followed_by, we would get

   w,L \non R followed_by P
   iff  w,L \non not(R |-> not P)
   iff  w,L \non R |-> not P
   iff  w,L \non R |-> P

Best regards,

John H.


> Here is an attempt to define when an assertion pass non-vacuously.
> This proposal is also available at mentis (1381).
> This is not a proposal, it's a definition for review and discussion.
> 
> There are a lot of vacuity definitions, I tried to have a simple definition
> that generalizes the implication vacuity that is already being used. The
> definition is on the structure of the property, on the property level, 
> meaning
> we have a new satisfaction relation. Let $\tight$ be the tight satisfaction
> relation, $\models$ the satisfaction relation and $\non$ the
> non-vacuous  relation. An attempt of a property $P$ on a suffix $w$
> pass non vacuously iff $w,{}\models P$ and $w,{}\non P$.
> 
> The definition of $\non$ is per attempt on a suffix $w$ of a computation.
> 
> Base: For every sequence $R$, property $P=R$, and assignment $L$, we 
> have that          
> $w,L\non P$.
> 
> Induction:
> 
>  * For $P =  (P_1)$ and assignment $L$, we have that $w,L\non P$  iff
>      $w,L \non P_1$.
> 
>  * For $P = R |-> P_1$ and assignment $L$, we have that $w,L\non P$  iff
>      there exists $i \geq 0$, and an assignment $L_1$ such that
>      $w^{0..i}, {}, L_1 \tight R$ and $w^{i..}, L_1\non P_1$.
> 
>  * For $P = P_1 and P_2$ and assignment $L$, we have that $w,L\non P$  iff
>      $w,L \non P_1$ or $w,L\non P_2$.
> 
>  * For $P = P_1 or P_2$ and assignment $L$, we have that $w,L\non P$  iff
>      $w,L \non P_1$ or $w,L\non P_2$.
> 
>  * For $P = not P_1$ and assignment $L$, we have that $w,L\non P$  iff
>      $w,L \non P_1$.
> 
>  * For $P = disable iff (b) P_1$ and assignment $L$, we have that 
> $w,L\non P$  iff
>      $w,L \non P_1$.
> 
> 
>