[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: Problem importing theories
This is a bug, could you please send your specs so I can try and fix it?
> 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
> IMPORTING T1[string,string]
> END T2
> Typechecking (with the command typecheck) reports the following error
> 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ť