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

Re: [PVS-Help] pvs raw mode



Boulifa,

There are two "batch" modes in PVS, pvs -raw and pvs -batch. The first one
is very basic (no Emacs support), the second one also runs Emacs in batch
mode. If you need support for text files, I would suggest "-batch". You
can always call CLISP code from ELISP and in ELISP you have all the Emacs
support you may need. See examples in the directory emacs/emacs-src of the
distribution. 

For examples of code where lemmas are instantiated with proof scripts and
then reran in batch mode, look at the directory src/ProofLite in the PVS
source code. The functionality provided by ProofLite is described here:

  http://shemesh.larc.nasa.gov/people/cam/ProofLite
 
Cesar

On 1/27/13 7:23 AM, "Boulifa Bilel" <boulifa.bilel@xxxxxxxxx> wrote:

>but I do not have a simple expression, what I want to do is start the
>proof of a theorem which is defined in a specific line in a file.
>I tried this function  " (rerun-proof-at? "file_systemTheorems" nil 6
>"pvs") "   but it returns me   "no"   and that's all.
>
>
>file_systemTheorems: is the file name
>6:is the line where the definition of theorem begins
>
>
>after that I did some research into the source code and I found in the
>file "pvs-lisp" the function "Prove-file-at" and I used the command "
>(prove-file-at" file_systemTheorems "nil 6)  "and it returns" Rule? "like
>"emacs" and then I was able to start the proof process.
>what do you think about it ?
>
>
>thank you very much for your help, it was very useful :)
>
>
>
>
>
>
>
>
>2013/1/24 MUNOZ, CESAR  (LARC-D320) <cesar.a.munoz@xxxxxxxx>
>
>Once you have type-checked a theory and the PVS context is set, you can
>use the Lisp function
>
>(simplify-expr <pvs-expr> :strategy <strategy>)
>
>where
>* <pvs-expr> is a CLOS object representing a *closed* PVS Boolean
>expression and
>* <strategy> is a PVS proof command.
>
>The function simplify-expr returns the PVS CLOS object that results from
>applying <strategy> to <pvs-expr>.
>
>To get a <pvs-expr> from a string, use the function
>
>(pc-parse "<something-in-pvs-syntax>" 'expr)
>
>You can try these functions in PVSio, which provides an interface to the
>PVS Lisp engine and to the PVS ground evaluator, e.g.,
>
><PVSio>  (simplify-expression (pc-parse "FORALL (x:real): x-x = 0" 'expr)
>:strategy '(grind))) !
>TRUE
>
>
>(The exclamation mark at the end of the line commands PVSio to evalute the
>Lisp expression).
>
>On the other hand
>
><PVSio> (simplify-expression (pc-parse "FORALL (x:real): x-x = 1" 'expr)
>:strategy '(grind))) !
>real_pred(x!1) IMPLIES 0 = 1
>
>If you download the PVS sources, go to the doc directory and look for the
>pvs-api draft. It documents some of these functions.
>
>Cesar
>
>--
>Cesar A. Munoz                             NASA Langley Research Center
>Cesar.A.Munoz@xxxxxxxx                     Bldg. 1220  Room 115 MS. 130
>http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
>Office: +1 (757) 864 1446 <tel:%2B1%20%28757%29%20864%201446>
>     Fax: +1 (757) 864 4234 <tel:%2B1%20%28757%29%20864%204234>
>
>
>
>
>On 1/24/13 3:20 AM, "Boulifa Bilel" <boulifa.bilel@xxxxxxxxx> wrote:
>
>>thank you for your response, it was very usefull now i can start pvs in
>>raw mode and put some rules but i can't start proof of a theorem, i can
>>put change-context and typecheck-file but how can i start proof of a
>>theorem and use rules to proove it like skosimp*, prop or grind ....?
>>
>>
>>
>>2013/1/21 Boulifa Bilel <boulifa.bilel@xxxxxxxxx>
>>
>>thank you very much, I'll take a look at this link and give you feedback
>>
>>
>>
>>2013/1/21 MUNOZ, CESAR  (LARC-D320) <cesar.a.munoz@xxxxxxxx>
>>
>>Boulifa,
>>
>>Look at the tool called Grizzly:
>>
>>http://shemesh.larc.nasa.gov/people/cam/Bernstein/Grizzly.html
>>
>>It is part of Bernstein in the NASA PVS Library (Try the version 5.0 of
>>the library, version 6.0 doesn't include Bernstein yet, but for what you
>>need it, it should be enough):
>>
>>
>>  http://shemesh.larc.nasa.gov/fm/ftp/larc/PVS-library/pvslib.html
>>
>>Grizzly is a script written in Perl that uses sockets to communicate with
>>PVS (running in raw mode).
>>
>>Regards,
>>
>>Cesar
>>
>>
>>On 1/21/13 3:44 AM, "Boulifa Bilel" <boulifa.bilel@xxxxxxxxx> wrote:
>>
>>>Does anyone have an example of using the pvs -raw mode?
>>>I'd like to use PVS from a Java program but i have not been able to
>>>invoke the pvs rules on command line.
>>>
>>>Thanks...
>>>
>>>--
>>>Best Regards
>>>
>>>Boulifa Bilel
>>>Computer Engineer
>>>
>>>
>>>Boulifa.Bilel@xxxxxxxxx
>
>
>>>Tel: (+216) 97 808 500 <tel:%28%2B216%29%2097%20808%20500>
>>><tel:%28%2B216%29%2097%20808%20500>
>>>       (+974) 33 52 24 90 <tel:%28%2B974%29%2033%2052%2024%2090>
>>><tel:%28%2B974%29%2033%2052%2024%2090>
>>>
>>>
>>>
>>>
>>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>--
>>Best Regards
>>
>>Boulifa Bilel
>>Computer Engineer
>>
>>
>>Boulifa.Bilel@xxxxxxxxx
>>
>
>>Tel: (+216) 97 808 500 <tel:%28%2B216%29%2097%20808%20500>
>><tel:%28%2B216%29%2097%20808%20500>
>>       (+974) 33 52 24 90 <tel:%28%2B974%29%2033%2052%2024%2090>
>><tel:%28%2B974%29%2033%2052%2024%2090>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>
>>--
>>Best Regards
>>
>>Boulifa Bilel
>>Computer Engineer
>>
>>
>>Boulifa.Bilel@xxxxxxxxx
>>Tel: (+216) 97 808 500 <tel:%28%2B216%29%2097%20808%20500>
>>       (+974) 33 52 24 90 <tel:%28%2B974%29%2033%2052%2024%2090>
>>
>>
>>
>
>
>
>
>
>
>
>
>
>-- 
>Best Regards
>
>Boulifa Bilel
>Computer Engineer
>
>
>Boulifa.Bilel@xxxxxxxxx
>Tel: (+216) 97 808 500
>       (+974) 33 52 24 90
>
>
>