~/reftool). Uncompress the archive using
gzip -d reftool.tar.gzand expand the archive using
tar -xvf reftool.tarThis creates a subdirectory
rt-pvs containing the theories and strategies and a subdirectory rt-tcl containing the Tcl/Tk code for the interface. The current directory will contain the Emacs-Lisp file rc_tcl_pipe.el and the README file.
RC_INTERFACE to the path that contains the interface; if you are using the C-shell and the path is ~/reftool/rt-tcl then add the following to .cshrc:
setenv RC_INTERFACE ~/reftool/rt-tcl
rc_tcl_pipe.el to some directory (e.g. ~/elisp) and add the following to .pvsemacs:
(load "rc_tcl_pipe")in case this file isn't found, insert the following line to
.pvsemacs before loading rc_tcl_pipe
(setq load-path (cons (expand-file-name "~/elisp") load-path))
rc_tcl_pipe.el contains the definition of an Emacs-Lisp function x-show-ref-prog used for starting the user interface of our refinement tool from within Emacs.
This function as well as the user interface uses the environment variable RC_INTERFACE to locate the interface code.
rt-pvs created in step 1 above.
Open the file rc_bag_ex.pvs which contains an example specification.
Start the prove-checker for the specification spec2. Do not rerun the proof. When starting the prover PVS should report that it defines several strategies.
In the initial goal do a (SKOSIMP).
Now start the user interface by
M-x x-show-ref-progA separate window with title `refinement tool' should appear. If this does not work look at buffer
if-buffer for error-messages. Check if Tcl/Tk (versions 7.4/4.0 or higher) is installed on your system and make sure that the environment variable RC_INTERFACE is set properly.
To check the Tcl version enter the unix command tclsh in a shell and enter puts $tcl_version at the %-prompt of Tcl; leave Tcl with exit; this should look like
sokrates{jkm} tclsh
% puts $tcl_version
7.4
% exit
sokrates{jkm}
where the unix shell prompt in this case is sokrates{jkm}. The Tk-version can be checked similarly:
sokrates{jkm} wish
% puts $tk_version
4.0
% exit
sokrates{jkm}
If the user interface is displayed you can click onto the button `From PVS' in the lower left corner of the window. This should insert two prover commands into buffer *pvs* and execute them. After some seconds the upper text window labeled `Current Program' should contain the following:
PROGRAM
VAR
l : list[real] ;
av : real
BEGIN
IF cons?(l)
THEN
{ cons?(l) } av := mean(l)
ELSE
SKIP
END-IF
END
If all this works properly, you have installed the tool successfully!
Use the save-context command of PVS to create the .bin files. Otherwise PVS type-checks all the theories whenever invoking the prover.