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

Help needed for learning PVS

Dear Respected PVS Users,

I am learning PVS, working on Version 2.2. Refer to Chapter 2 of PVS
System Guide. I am trying to work on the simple example of sum.pvs
given in the Examples directory, which gives a specification of the
sum of the first n natural numbers. However, I have encountered errors
which I am unable to follow. 
I opened the PVS window, introduced the sum theory into the working
directory of pvs by copying the file from Examples directory. After the
sum specification is displayed in the current buffer, I invoke the parser
by giving the command "M-x pa". But an error appears, which I cannot make
out. In the current buffer, it is written 
"--:-- sum.pvs [(PVS: error)]--L14--Bot -----
SPC-scroll, I-ignore, K-keep, A-abort sends and keep or B-break:" 
and another buffer opens up on top of the current buffer saying
"-1:-- *scratch* [(Lisp Interaction)]--L1-All----
Error: attempt to call `PARSE-FILE' which is an undefined function."

Please suggest how to proceed after this.

	With best regards, Indrajit Chakrabarti

p.s. Please send a copy of your reply to the email address

 Indrajit Chakrabarti                      |
 Assistant Professor                       |
 Department of Electronics                 |
 and Communication Engg.                   |
 Indian Institute of Technology, Guwahati  |tel: +91 361 690321-328 (8 lines)
 North Guwahati,                           |extn. 2060, 2056 (ECE office)       
 Guwahati - 781 039                        |fax: +91 361 690762     
 Assam,  INDIA.                            |email:indra@iitg.ernet.in,
                                           |      indrac@postmark.net
Please send your reply to both the above email addresses.