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

Problem importing theories



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ť