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

Re: [PVS-Help] Error: No Method Applicable for Generic Function



Hi--

<Cesar>

I tried your approach and I still got the same error 

</Cesar>

Then I tried something. Recall originally I had,

theory1: THEORY
begin
  
   IMPORTING foo@theory2
   
   ...
   ...

end theory1

theory2 is located in foo

theory2: THEORY
begin

	IMPORTING foobar@theory3

        ...
        ...
end theory2

which means that in theory1, theory3 should be imported. At this point I still 
had the error. Then just for the sake of experimenting I modified theory1 as 
follows

theory1: THEORY
begin
  
   IMPORTING foo@theory2,foobar@theory3
   
   ...
   ...

end theory1

theory2 still imports theory3 and now theory1 imports both theory2 and 
theory3. Somehow PVS was able to typecheck the modified theory1.

Why should I import theory3 in theory1 when it is already imported in theory2?

rgds
-NDK

--
http://engr.smu.edu/~nikhil

On Wednesday 08 March 2006 04:04 pm, you wrote:
> IMHO this is a better approach:
>
> 1. Define the environment variable PVS_LIBRARY_PATH:
>
> PVS_LIBRARY_PATH=:<fooroot>
>
> where <fooroot> is the full path to the root of foo, i.e.,
>
> $ test -d <fooroot>/foo && echo Yes
>
> should print Yes.
>
> 2. Remove lib:LIBRARY = "foo/" from theory1 and import theory2 as
> follows:
>  IMPORTING foo@theory2
>
> 3. Done.
>
> Cesar

-- 
You never hesitate to tackle the most difficult problems.