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

[PVS-Help] strange mapping when loading library files twice

Dear All,

Not sure whether you have encountered this interesting situation before (at least I don't find the question/solution about it from the archive). In this email, I would like to share what happened and what is the possible solution. Your any comments are gratefully welcome.

I am using PVS 3.2 in the UNIX system. I have set the library path correctly two weeks before. Today when I tried to prove some theories which have been validated two months ago, something strange happened: the prover can find the lemma name (say "A") from the library files, but it displayed contents of other lemma (say "B"). More details are below:

1. A PVS file (say "P.pvs") contains a set of lemmas such as "A" and "B", and is located in the library folder (say "lib").
2. A PVS file (say "T.pvs") contains a theory and imports the library file, i.e., P.pvs by the statement "importing lib@P;".
3. When proving, we want to apply lemma "A" by the command "(lemma "A")". However, the prover shows the content of lemma "B".

Methods I have tried to solve the strange mapping:
1. Remove the backup files of T.pvs, i.e., "T.pvs~" and "T.prf~", but it didn't work.
2. Remove the bin file of T.pvs, i.e ., "T.bin" in the sub-foler "pvsbin", but it didn't work.
3. Remove the statement "importing lib@P" from T.pvs, and it WORKS.

My guess: Something wrong when loading PVS library files twice.
Reason of my guess: after I set the library path correctly, the PVS prover would load all files in the folder "lib" initially. when I open the file, "T.pvs" and start a proof, the prover would load the library file " P.pvs" again due to the statement "importing lib@P". Hence, "P.pvs" has been loaded twice, and it may cause the mapping between lemma names and the contents incorrect.

The above is my experience, and I would like to hear more from you such as whether I have done something wrong, etc.


Chunqing CHEN
Research Assistant
Computer Science
School of Computing
National University of Singapore