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

Re: Problem importing theories



Hello Maria,

This is a bug, could you please send your specs so I can try and fix it?

Thanks,
Sam Owre

> Hello:
> 
>    I have a problem importing theories in PVS. Assume that we have a 
> theory T1 with non-interpreted types R and D as parameters. This theory 
>    contains specifications of some algorithms and it has been proved 
> using the command "prove-importchain".
> 
>    I want to instantiate this theory T1 for a given pair of interpreted 
> types (like strings or naturals, for example) in order to execute the 
> algorithms using the PVS-ground-evaluator. For example:
> 
> T2: THEORY
>    BEGIN
>      IMPORTING T1[string,string]
>    END T2
> 
> Typechecking (with the command typecheck) reports the following error 
> message:
> 
> Error: the assertion itheory failed
> 
> I have been trying to see why this error occurs, but I have not found it 
> in the documentation.
> 
>   Thanks in advance for your help.
> 
> Maria Josť
>