Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|

Synopsis: load-prelude-library theory invisible without importings Severity: serious Priority: medium Responsible: owre State: analyzed Class: sw-bug Arrival-Date: Tue Jul 31 19:05:00 2001 Originator: Ben L. Di Vito Organization: larc.nasa.gov Release: PVS 2.3 Environment: System: Architecture: Description: First I created a test directory and included a subdirectory "extend" having the following PVS file: extra_real_props: THEORY BEGIN w, x, y, z: VAR real n0w, n0x, n0y, n0z: VAR nonzero_real nnw, nnx, nny, nnz: VAR nonneg_real pw, px, py, pz: VAR posreal npw, npx, npy, npz: VAR nonpos_real nw, nx, ny, nz: VAR negreal div_cancel4: LEMMA x = y/n0z IFF x * n0z = y zero_times4: LEMMA 0 = x * y IFF x = 0 OR y = 0 END extra_real_props Then I typechecked extra_real_props and exited to save the context (in "extend"). Next I restarted PVS (in the parent directory) and typechecked the following test file: test : THEORY BEGIN a,b,c : real t1 : LEMMA a = b/c END test I invoked M-x load-prelude-library and gave it the path for extend. This worked fine. Then I started a proof of t1 to produce the following error, in which the prover is unable to find the lemma div_cancel4. t1 : |------- {1} a = b / c Rule? (lemma "div_cancel4") Couldn't find a definition or lemma named div_cancel4Expecting a formula or c onstant No resolution for div_cancel4 No change on: (LEMMA "div_cancel4") Then I edited the theory as follows to add a superfluous importing statement: test : THEORY BEGIN IMPORTING real_props a,b,c : real t1 : LEMMA a = b/c END test This caused the prover to behave as expected on the next attempt: t1 : |------- {1} a = b / c Rule? (lemma "div_cancel4") Applying div_cancel4 this simplifies to: t1 : {-1} FORALL (n0z: nonzero_real, x, y: real): x = y / n0z IFF x * n0z = y |------- [1] a = b / c Even more curious is that when I restarted PVS after deleting the context file and used the following alternative version of the test theory, the proof step failed in the same way. In other words, the importing statement didn't solve the problem in this case. test2 : THEORY BEGIN IMPORTING real_props a,b,c : real t1 : LEMMA a = b/c END test2 How-To-Repeat: Fix: The context is in some cases ignoring the prelude libraries. Fixed decl-context to do the right thing.

Home | • | Intro | • | Announce | • | FAQ | • | Docs | • | Download | • | • | Status | • | Bugs | • | Users | • | Related | • | FM Tools |
---|