RE: [sv-ac] vacuity

Hi Doron,

I like it, simple. Questions:

- for "not", this will define non-vacuous failure if used alone in an
assert.
- for "disable iff", how is b taken into account? 

For practical purpose, would it be useful to defined the dual relation
"vacuous" directly rather than through "not non" ? E.g., for
implication:
$P = R |-> P_1$ and assignment $L$, we have that 
 $w,L\vac P$  iff
      for all $i \geq 0$, and assignments $L_1$ such that
      $w^{0..i}, {}, L_1 NOT\tight R$ or 
      $w^{0..i}, {}, L_1 \tight R$ $w^{i..} and L_1\vac P_1$.

Best regards,
ed

> -----Original Message-----
> From: owner-sv-ac@eda.org [mailto:owner-sv-ac@eda.org] On 
> Behalf Of Doron Bustan
> Sent: Thursday, March 30, 2006 2:15 PM
> To: sv-ac@eda.org
> Subject: [sv-ac] vacuity
> 
> 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$.
> 
> 
> 
>