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

[PVS-Help] about nasalib




Hello everyone:

When I using nasalib prelude file (availabe in http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html ) in PVS 5.0 under the emacs interface  using Ubuntu 10.10 .

When I typecheck the file  ".../nasalib/structures/top.pvs", In  *Message* Buffer  give us the following meesage:

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Type-error in KERNEL::OBJECT-NOT-TYPE-ERROR-HANDLER:  NIL is not of type (OR BASE-STRING FILE-STREAM PATHNAME)
   [Condition of type TYPE-ERROR]
Restarts:
  0: [ABORT] Return to debug level 5.
  1:         Return to debug level 4.
  2:         Return to debug level 3.
  3:         Return to debug level 2.
  4:         Return to debug level 1.
  5:         Return to Top-Level.
Debug  (type H for help)
(MERGE-PATHNAMES 1 NIL "Library ints/ does not exist" NIL)[:EXTERNAL]
Source: Help! 11 nested errors.  KERNEL:*MAXIMUM-ERROR-DEPTH* exceeded.
Debug  (type H for help)
(DEBUG::DEBUG-LOOP)
Help! 12 nested errors.  KERNEL:*MAXIMUM-ERROR-DEPTH* exceeded.
Debug  (type H for help)
(DEBUG::DEBUG-LOOP)
Source:
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

If  I run the  command line 
../provethem nasa.all

to the  "nobin" lib file

system give me the hints: 

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
xu@ubuntu:~/PVS5.0/nasalib$ ../provethem nasa.all 
Processing nasa.all. Output in ./nasa.summaries
PVS_LIBRARY_PATH=home/xu/PVS5.0/nasalib
ints                     [Help! 12 nested errors.  KERNEL:*MAXIMUM-ERROR-DEPTH* exceeded.
Debug  (type H for help)
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++


Some other pvs file also give the similar messages 

In MinBuffer   the following message shows

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
SPC-scroll, I-ignore, K-keep, A-abort sends and keep or B-break:  
Restart
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

 typecheck   the pvs file  ".../nasalib/ints/top.pvs",   we have the following messages

++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
Making completion list...
Typechecking top
Parsing div
div parsed in 0.07 seconds
Typechecking div
Parsing floor_div_lems
floor_div_lems parsed in 0.01 seconds
Typechecking floor_div_lems
floor_div_lems typechecked in 0.25s: No TCCs generated
Parsing abs_rews
abs_rews parsed in 0.00 seconds
Typechecking abs_rews
abs_rews typechecked in 0.03s: No TCCs generated
div typechecked in 1.55s: 6 TCCs, 0 proved, 1 subsumed, 5 unproved
Parsing rem
rem parsed in 0.02 seconds
Typechecking rem
rem typechecked in 0.63s: 2 TCCs, 0 proved, 0 subsumed, 2 unproved
Parsing mod_div_lems
mod_div_lems parsed in 0.00 seconds
Typechecking mod_div_lems
mod_div_lems typechecked in 0.29s: No TCCs generated
Parsing mod_lems
mod_lems parsed in 0.02 seconds
Typechecking mod_lems
mod_lems typechecked in 0.82s: 1 TCC, 0 proved, 0 subsumed, 1 unproved
Parsing gcd
gcd parsed in 0.04 seconds
Typechecking gcd
Parsing divides_lems
divides_lems parsed in 0.02 seconds
Typechecking divides_lems
Parsing max_bounded_posnat
max_bounded_posnat parsed in 0.02 seconds
Typechecking max_bounded_posnat
max_bounded_posnat typechecked in 0.37s: 5 TCCs, 0 proved, 0 subsumed, 5 unproved
divides_lems typechecked in 0.66s: 1 TCC, 0 proved, 0 subsumed, 1 unproved
gcd typechecked in 1.74s: 23 TCCs, 0 proved, 13 subsumed, 10 unproved
Parsing gcd_fractions
gcd_fractions parsed in 0.01 seconds
Typechecking gcd_fractions
gcd_fractions typechecked in 0.29s: 7 TCCs, 0 proved, 4 subsumed, 3 unproved
Parsing tdiv
tdiv parsed in 0.03 seconds
Typechecking tdiv
tdiv typechecked in 0.93s: 4 TCCs, 0 proved, 0 subsumed, 4 unproved
Parsing tmod
tmod parsed in 0.03 seconds
Typechecking tmod
tmod typechecked in 1.80s: 2 TCCs, 0 proved, 0 subsumed, 2 unproved
Parsing div_nat
div_nat parsed in 0.13 seconds
Typechecking div_nat
Parsing floor_more
floor_more parsed in 0.00 seconds
Typechecking floor_more
floor_more typechecked in 0.06s: No TCCs generated
div_nat typechecked in 0.69s: 2 TCCs, 0 proved, 0 subsumed, 2 unproved
Parsing mod_nat
mod_nat parsed in 0.02 seconds
Typechecking mod_nat
Mark set
mod_nat typechecked in 0.61s: 1 TCC, 0 proved, 0 subsumed, 1 unproved
Parsing primes
primes parsed in 0.01 seconds
Typechecking primes
primes typechecked in 0.02s: No TCCs generated
Parsing factorial
factorial parsed in 0.01 seconds
Typechecking factorial
factorial typechecked in 0.28s: 8 TCCs, 0 proved, 1 subsumed, 7 unproved
Parsing product
product parsed in 0.07 seconds
Typechecking product
Mark set
product typechecked in 1.57s: 39 TCCs, 0 proved, 11 subsumed, 28 unproved; 2 warnings
Parsing product_below
product_below parsed in 0.01 seconds
Typechecking product_below
product_below typechecked in 0.32s: 8 TCCs, 0 proved, 0 subsumed, 8 unproved
Parsing product_int
product_int parsed in 0.01 seconds
Typechecking product_int
product_int typechecked in 0.60s: 1 TCC, 0 proved, 0 subsumed, 1 unproved; 2 warnings
Parsing product_nat
product_nat parsed in 0.03 seconds
Typechecking product_nat
product_nat typechecked in 0.61s: 23 TCCs, 0 proved, 10 subsumed, 13 unproved
Parsing product_posnat
product_posnat parsed in 0.01 seconds
Typechecking product_posnat
product_posnat typechecked in 0.49s: 12 TCCs, 0 proved, 4 subsumed, 8 unproved
Parsing product_upto
product_upto parsed in 0.02 seconds
Typechecking product_upto
product_upto typechecked in 0.31s: 11 TCCs, 0 proved, 3 subsumed, 8 unproved
top typechecked in 14.84s: No TCCs generated
++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++

Why?



2011-05-28 
 QG XU