[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS-Help] Annoying TCCs



Hi Sjaak,

I was able to prove all the TCCs using a preserves? function (this might
be a nice one for the datatype mechanism to generate automatically):

Test [V:TYPE]: THEORY
BEGIN
AT: TYPE = { strict, lazy }

IMPORTING TYPES[V,AT]

preserves?(t: TYPES)(tt: TYPES): bool =
      (st?(t) => st?(tt))
  AND (t_var?(t) => t_var?(tt))
  AND (t_arr?(t) => t_arr?(tt))
  AND (t_unit?(t) => t_unit?(tt))
  AND (t_pair?(t) => t_pair?(tt))
  AND (t_sum?(t) => t_sum?(tt))

lazy(t: TYPES) : RECURSIVE (preserves?(t))
  = CASES t OF
       st(ta,tt) : st(lazy,lazy(tt)),
       t_var(i) : t_var (i),
       t_arr(a,r) : t_arr (a,r),
       t_unit : t_unit,
       t_pair(x,y) : t_pair(lazy(x),lazy(y)),
       t_sum(l,r) : t_sum(lazy(l),lazy(r))
    ENDCASES
 MEASURE t BY <<;

END Test

This generates 16 TCCs, but 11 are discharged by M-x tcp, and the rest are
of the form

("" (skosimp :preds? t) (typepred "v!1(r!1)") (grind))

Regards,
Sam

Sjaak Smetsers <s.smetsers@science.ru.nl> wrote:

> Hi,
> 
>  
> 
> I?ve defined the following data type:
> 
>  
> 
> TYPES[V,A:TYPE]: DATATYPE WITH SUBTYPES ST, PT
> 
> BEGIN
> 
>                 st (att:A,pt:PT)                 : st?                       :
> ST
> 
>  
> 
>                 t_var (id:V)                        : t_var?               
>                 : PT
> 
>                 t_arr(arg:ST,res:ST)        : t_arr?                 : PT
> 
>                 t_unit                                   : t_unit?             
> : PT
> 
>                 t_pair (x,y:ST)                   : t_pair?               : PT
> 
>                 t_sum (l,r:ST)                    : t_sum?              : PT
> 
> END TYPES
> 
>  
> 
> And a simple recursive function named ?lazy?:
> 
>  
> 
> Test [V:TYPE]: THEORY
> 
> BEGIN
> 
> AT: TYPE = { strict, lazy }
> 
> IMPORTING TYPES[V,AT]
> 
>  
> 
> lazy(t:TYPES) : RECURSIVE TYPES
> 
> = CASES t OF
> 
>                                st (ta,tt)               : st(lazy,lazy(tt)),
> 
>  
> 
>                                t_var (i)               : t_var (i),
> 
>                                t_arr (a,r)            : t_arr (a,r),
> 
>                                t_unit                   : t_unit,
> 
>                                t_pair (x,y)         : t_pair(lazy(x),lazy(y)),
> 
>                                t_sum (l,r)          : t_sum(lazy(l),lazy(r))
> 
>                 ENDCASES
> 
> MEASURE t BY <<;
> 
> END Test
> 
>  
> 
> This definition causes PVS to generate a number of TCCs which I can?t prove.
>  In essence these TCCs try to enforce that the recursive call to lazy
> 
> produces an expression of the right subtype, which is obviously the case.
> 
>  
> 
> How do I get rid of these annoying TCCs?
> 
>  
> 
> Thanks,
> 
> 
> Sjaak