PVS API

From SRI PVS
Jump to: navigation, search

Running PVS Standalone (without Emacs)

Running PVS without Emacs is done with the -raw flag. This section describes how to make effective use of PVS when run in this way.

Interaction

When run in standalone mode, PVS acts as a unix pipe, taking input on stdin and writing output to stdout, ith error messages to stderr. Normally PVS reads input, processes it, writes the result, and prompts for more input. The Emacs interface works in this way, and it is worth looking at the Emacs sources in PVS/emacs/emacs-src for guidance. If this is being done by a separate process, it should recognize the prompt, so that it knows when PVS is finished with the current task.

The prompts you should handle are given by the Emacs regular expression comint-prompt-regexp in PVS/emacs/emacs-src/pvs-ilisp.el. This changes for different underlying Lisps. All of the prompts listed below are followed by a space.

The basic prompt is

Allegro 
pvs(27):
CmuLisp 
*

In a break loop, the prompt is

Allegro 
[1] pvs(28):
CmuLisp 
0]

The Allegro prompt sometimes includes a c, e.g., [1c] pvs(28): ). The number inside the square bracket(s) indicates the break level, it is incremented if a break occurs within a break. A break means that lisp has suspended processing at this point, so that the cause of the break may be investigated. Unless you caused the break (e.g., by interrupting the prover), this usually indicates there is a problem, and should be investigated. If you want your program to ignore the break, send

Allegro 
:reset
CmuLisp 
continue

to unwind the break to the top level.

The prover, ground evaluator, and PVSio all have their own prompts:

Prover 
Rule?
Ground evaluator 
<GndEval>
PVSio 
<PVSio>

Note that if an error is encountered while interacting with the prover or the ground evaluator, the prompt reverts to the break prompt described above. In this case :reset (for Allegro) or continue (for CmuLisp) will end the prover, ground evaluator, or PVSio interaction, while (restore) returns control.

Invoking the typechecker and prover

See the comments in PVS/src/raw-api.lisp for details.

Personal tools