PVS‎ > ‎

@ get started

PVS is currently available at ENSEIRB-MATMECA on ssh.enseirb-matmeca.fr Linux machine, at the following location

/usr/local/pvs/5.0/pvs

This command actually launches Emacs augmented with PVS commands as a detached process.

PVS can also be installed on a laptop under Linux or Mac OS X (including Lion, with some difficulty though...) and even Windows.
Getting started on a simple example
In order to run PVS on this machine, you are advised to take the following steps:
  1. ssh -Y ssh.enseirb-matmeca.fr   # connect to ssh machine
  2. cd                              # root of your account
  3. mkdir pvs                       # if necessary (first time)
  4. cd pvs
  5. mkdir intro                     # create this directory for initiation purposes
  6. cd intro                        # go there before launching PVS
  7. Copy first_steps.dmp.txt PVS dump into your intro directory.
  8. /usr/local/pvs/5.0/pvs          # launch PVS from this context
  9. Once PVS is started, you see a Welcome buffer within Emacs window, and restore theories and proofs by typing:
    • <Meta-x>undump-pvs-files<Return>
    • first_steps.dmp.txt<Return>         # when prompted for the name of the PVS dump
    • <Return>                            # to accept undumping into your "intro" directory
  10. Load the first_steps theory in a new buffer by using the following PVS command:
    • <Ctrl-c><Ctrl-f>first_steps<Return> # never use <Ctrl-x><Ctrl-f> Emacs command!
  11. Follow the advice in first_steps leading comments inviting you to load and focus on propositional theory.
Useful tip
It is convenient to define pvs as a symbolic link in each PVS context (directory), such as intro, you will use for exercises or for your project:
ln -s /usr/local/pvs/5.0/pvs pvs
Then you just have to type
./pvs
from the relevant PVS context (directory), in order to launch PVS from this context.
About dumps and PVS directories
A PVS dump is a unique text file corresponding to a snapshot of all your theories and proofs contained in a PVS directory (also called PVS context, or PVS library). A dump is thus a convenient means of representing the comprehensive state of your theories and proofs in a given directory, and sharing it with other people. There is a "root theory" in every dump: the root theory directly or indirectly imports all other theories. For instance, the first_steps theory in the simple example below imports the propositional and f91 theories among others. Before producing a dump, it is important to type check your root theory; otherwise, your dump will be incomplete.
In this class, we generally use a precise scheme to name a dump:
5.0.context.date_and_time.root.dmp.txt
where
  • 5.0 refers to the PVS version used to produce the dump;
  • context is the name of your PVS directory in which theories and proofs were performed;
  • date_and_time specifies the time of production of your dump, e.g. 25oct2013, or 25oct2013at19h35, if you have produced more than one dump this day;
  • root is the name of your root theory;
  • dmp.txt is a suffix representative of a dump, the txt being added for compatibility with Google Drive viewer.
According to this convention, the above first_steps.dmp.txt PVS dump should rather have been named:

5.0.intro.18sep2013.first_steps.dmp.txt

Although it is also possible to produce a more complex dump (called inclusive) representing several directories (libraries), in the case where some libraries depend upon other ones, it is not a good idea in practice: you are advised to produce only simple dumps, not inclusive dumps. Beware of the terminology:

PVS directory = PVS context = PVS library = set of theory files and proof files

A theory file, such as theory_name.pvs, usually corresponds one and one only theory identified by its name: theory_name; the proofs associated with a theory are automatically stored in a unique file named theory_name.prf. You should not edit proof files.


ċ
first_steps.dmp.txt
(9k)
Paul Y Gloess,
18 sept. 2013, 10:59
v.2
Comments