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

[PVS-Help] Annoying TCCs



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