PVS version 7.1 and the development version of the NASA PVS Library are required to use the PVS development provided with the PRECiSA distribution.
To type-check and prove the PRECiSA development in PVS for the first
time, type the following
command in a Unix shell within the local directory PVS.
$ provethem
The output of that command is
PRECiSA [OK]
*** Number of libraries: 1
*** Grand Totals: 126 proofs / 126 formulas. Missed: 0 formulas.
To proof-check the symbolic certificates generated by PRECiSA in
PVS, the local directory PVS has to be added to the Unix environment variable
PVS_LIBRARY_PATH. Depending upon your shell, one of the following lines
has to be added to your startup script. In C shell (csh or tcsh), put this line in
~/.cshrc, where <precisapvsdir> is the absolute path to the local
directory PVS in the PRECiSA distribution:
setenv PVS_LIBRARY_PATH "<precisapvsdir>:$PVS_LIBRARY_PATH"
In Borne shell (bash or sh), put this line in either ~/.bashrc or ~/.profile:
export PVS_LIBRARY_PATH="<precisapvsdir>:$PVS_LIBRARY_PATH"