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

[PVS-Help] PVS 4.1 Errors



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