Re: [PVS-Help] PVS 4.1 Errors

[Sam Owre <owre@xxxxxxxxxxx>]

Hi Jim,

This is a bug in PVS - could you please send me your specs, so that we
can get this fixed?

Thanks,
Sam Owre

jim armstrong <armstrong.jm@xxxxxxxxx> wrote:

> Hi,
> 
> Can anyone there tell me what the following errors are:
> 
> A)      error: no methods applicable for generic function
> 
> 
> B)        break: repeated bindings in make-subtype-tcc-decl
> 
> 
> 
> A  occurs whilst "tcp" is running proofs of proof obligations, but I've had it
> occur in proofs
> 
> done in previous versions of PVS that I have re-installed. It appears to be
> emitted by "grind".
> 
> It looks like some sort of lisp error. Doing the proofs again step by step gets
> rid of it altogether.
> 
> 
> 
> B is a total mystery to me:  it occurs when type-checking. It is provoked by
> certain type declarations. 
> 
> You can comment bits out to discover which declarations. These declarations
> look fine (e.g. they parse ok),
> 
> but they are always dependent-type declarations where certain fields are
> function types.
> 
> 
> I re-jigged one declaration that was causing B and simplifying things
> mysteriously got rid of it.
> 
> But then when I declared a constant of said type, B returns when
> PVS type-checks that constant.
> 
> 
> B worries me the most, since either a declaration is type-correct or it isn't.
> It can raise tccs but I don't see how no
> 
> tccs (provable or otherwise) can be defined for it.
> 
> 
> thanks in advance
> 
> 
> jim