PVS is a formal specification language and prover. It is used in real groups and projects, e.g., the NASA Langley group.
On the Prism computers you can start PVS with: /cs/home/lai/pvs-4.2/pvs
Create new file: PVS menu → Files and Theores → new-pvs-file, then enter name (without the .pvs suffix).
Load file: PVS menu → Files and Theores → find-pvs-file, then enter name (without the .pvs suffix). Keyboard: ctrl-c ctrl-f
Save file: PVS menu → Files and Theores → save-pvs-file. Keyboard: ctrl-x ctrl-s. Also the save button in the toolbar.
Parse, typecheck: PVS menu → Parsing and Typechecking → etc. If you ask for typechecking, parsing will also be done. Keyboard: ctrl-c ctrl-t for typechecking.
Prove (one statement): PVS menu → Prover Invocation → prove. This will parse and typecheck first, then start a proof session for the statement near the cursor. If it has been proved previously, you will be asked several questions about whether you want to re-use the previous proof or write a new proof. Keyboard: ctrl-c p
If the prover goes into an infinite loop, press ctrl-c ctrl-c, then you will get a strange message and prompt, then enter :reset, that will bring it back to normal.
Exit: ctrl-x ctrl-c, or close the window.
Proofs are saved in files with the extension .prf, e.g., if your PVS file is X.pvs, proofs are saved in X.prf.
Emacs tidbits:
Sample file. (Updated May 12.)
Keywords and operators are case-insensitive, e.g., THEORY=theory, FORALL=forall. Names are case-sensitive.
name : THEORY BEGIN stuff END name demo : THEORY BEGIN stuff END demo
A theory is like a module. The above example defines a theory and calls it "demo". Put all your stuff inside a theory. You can have several theories in the same file (but no nesting).
A comment begins with % and extends to the end of line.
name : THEOREM statement imp : THEOREM forall (x:int): exists (x1:int): not (x=0 & x1>=x)
This assigns the name "imp" to a statement to be proved. Statements to be proved are marked by CHALLENGE, CLAIM, CONJECTURE, COROLLARY, FACT, FORMULA, LAW, LEMMA, PROPOSITION, SUBLEMMA, THEOREM. (Same meaning. Lower case also works because these are keywords.)
name : type = value max_size : nat = 10 name(params and types) : result type = body f(n:nat, b:bool) : nat = if b then n+1 else n*2 endif name(params and types) : RECURSIVE result type = body MEASURE expression zero(n:nat) : RECURSIVE nat = if n>0 then zero(n-1) else 0 endif MEASURE n
These define constants and functions. Recursive functions require special treatment: The idea is that you have to tell PVS why the recursion terminates, and you do this by pointing out an expression that decreases across recursive calls and is non-negative.
You can also specify constants and functions without values if the values do not matter:
name : type N : nat F : [nat -> nat]
Writing variables with their types everywhere can become tedious, especially when you define a function and then state a lot of properties of that function, e.g.,
f(n:nat) = n+10 T0 : THEOREM forall (n:nat): n>=0 T1 : THEOREM forall (n:nat): n>=1 T2 : THEOREM forall (n:nat): n>=2
To avoid writing n:nat repeatedly, you can do this:
n : VAR nat f(n) = n+10 T0 : THEOREM forall n: n>=0 T1 : THEOREM forall n: n>=1 T2 : THEOREM forall n: n>=2
Beware that it does not create a "global variable" in the programming sense! All it means is: whenever you define a function with parameter n or write a quantified statement with bound variable n, you can just write n and PVS expands it to n:nat. It just enables a shorthand.
Basic types: bool, nat, int, rat, real, number_field
Function type: [type -> type]
arrays and lists: finite_sequence[item type] e.g., finite_sequence[bool] is the type of arrays of booleans.
Subtypes (restricting a type to a condition): You do not have to say your variable has type nat; you can actually say your variable has type being those natural numbers strictly less than 10, or in general take any existing type and impose an extra condition. The long form is:
{ v : type | condition on v }
{ n:nat | n < 10 }
Beware that v is just for the sake of specifying the condition inside and does not "leak" outside. For example n in the example has nothing to do with any occurrence of n elsewhere.
Here are some examples in various contexts:
N:{n:nat|n<10} declares a constant natural less than 10.
F:[{n:nat|n<10} -> {n:nat|n<5}] declares a function mapping
naturals less than 10 to naturals less than 5.
f(n : {n:nat|n>=1}) : {m:nat|m>=2} = n+1 defines a function and
is very specific about its domain and co-domain.
silly : THEOREM forall (x : {x:int|x>=-10}): x+1>=-9
For all integers x at least -10, x+1 is at least -9.
In function parameters and quantified variables, the notation
(v:{v:type|cond}) is tedious and redundant; therefore a shorthand
is allowed: (v:type|cond). Examples:
f(n:nat|n>=1) : {m:nat|m>=2} = n+1
(There is no shorthand for result types.)
silly : THEOREM forall (x:int|x>=-10): x+1>=-9
The most interesting thing happens when a parameter's type depends on
previous parameters. Here is a motivation: define a recursive function
for the sum of an array from one index to another:
sum(L:finite_sequence[real], i:?, j:?) : RECURSIVE real = ...
What should be the types of i and j? It is not very nice to just make them
nat's, since arbitrary indexes may be invalid. Here is a solution:
you can say that i is at most L`length, and j is
between i and L`length:
sum(L:finite_sequence[real], i:nat|i<=L`length, j:nat|i<=j & j<=L`length) : RECURSIVE real = ...
And so the type of i depends on the value of L, and the
type of j depends on the values of both i and L.
Because types in PVS are so flexible, the typechecking phase creates extra statements to be proved. Example: if you mention L`seq(n), PVS wants you to prove 0≤n<L`length. Recursive definitions also create extra statements to be proved (your measure really decreases and is at least 0). To see them, use PVS menu → Viewing TCCs → show-tccs. Most of them can be proved automatically: use PVS menu → Parsing and Typechecking → typecheck-prove. Most people do it after major changes to their files but skip it for minor changes.
This is not a comprehensive list. Just the ones I use most often and adequate.