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

Re: [PVS-Help] importing another theory


Could you send me your PVS files?  "No next method" indicates a bug in
PVS, for which there is not a simple fix - it depends on the methods


sujith cs <cs_sujith@yahoo.com> wrote:

> Sir,
>    I am converting a program written in c language to typed transition system
> accepted by pvs theorem prover.a main program calls another procedure.
> For eg.
> Procedure rt(int x, int y)
> ……..
> …..
> X=dt(a,b)
> .
> I want to express this .
> I wrote two theories named rt and dt. when I tried to import dt in rt, an error
> message came “there is no next method for method” what is it.how to resolve it.