Literate PVS

This is my contribution to the "literate programming" thread; most recently Pertti Kellomäki mentioned it in this message to the PVS list.

What is "Literate PVS"? It's a method for including particular comments in a PVS file so that a literate PVS processor (LPP) can translate the PVS code plus comments into useful LaTeX files. Pertti's implementation uses strings defined in the PVS file, and has an LPP written in Python. My LPP is a perl hack, and it can:

The idea behind Literate PVS is that if you can write both code and suitably descriptive comments in one file - the PVS file - then it's less likely that the comments and the code will diverge. In addition, you could conceivably write an entire article on the formalization of some problem in PVS in one file: the PVS file. All your text would be there, and the LPP can convert this into a LaTeX file suitable for printing.

The rest of this page is technical stuff about how to apply Literate PVS in your files. You can skip it if the advertising blurb above doesn't grab yourattention.

Literate PVS syntax: Literate PVS uses comments for all processing instructions. There are three kinds of comments that affect when and where text is output:

In other words, in order to document a PVS file with text that can be converted to LaTeX, you put %%% in front of the documentation text. Any additional comments that are relevant for the PVS file but not for the LaTeX output can be added as single-percent comments. eg.:

	%%% This axiom adds an essential property of foos that
	%%% enables us to prove our primary theorem.
	% Yes, i know this is a hack
	foo : AXIOM false

The block mode is controlled by some additional comments. You use a comment of the form %+BEGIN to indicate that a block is beginning, and %+END to indicate that the block has stopped. Every block has a name which must be mentioned in the begin and end comments, much like PVS theories must BEGIN and END with a name. The name of the block determines the filename it is written to. It is an error to nest blocks. A single block can be separated within the PVS file; a second %+BEGIN with the same block name will append to the LaTeX output for that block.

	%%% This is text for file-mode.
	%+BEGIN gerbils
	gerbil : TYPE+
	male? : pred[gerbil]
	female?(g:gerbil) : bool = NOT male?(g)
	%+END gerbils

Applying the LPP to this will result in an output file called gerbils.tex (the name of the block) containing LaTeX code to typeset the PVS definitions within the block. Remember that single-percent comments will be typeset as normal text within blocks.

In file mode, sometimes there's uninteresting stuff in your PVS file. Test lemmas, for example, or lots of variable declarations that you're not interested in. You can %+IGNORE and %+RESUME output to effectively "comment out" pieces of PVS code for the file-mode processor.

Strip mode strips all comments and basically puts a \begin{PVS} \end{PVS} pair around the whole file.

Speaking of \begin{PVS}, the output of the LPP assumes that you are using the "pvs" package, so you will have to \usepackage{pvs} at the top of your LaTeX file that \includes the output of the LPP. The "pvs" package for LaTeX is my own package, available for download.

Finally, index mode makes a list of all the LEMMAs and THEOREMs in your file and outputs them at the end of processing as an itemized list (ie. \begin{itemize}). In addition, if you mark a definition with the special comment %PROP, it will be added to the list as well. You do need to follow some simple syntax rules for the index mode to work:

This is OK as well:

active?(a) : bool = EXISTS (s,s_) : Effect(s,a,s_) ; %PROP

My experience shows that the block mode is especially useful. You can use it to keep your PVS code in-sync with the article that describes it. You don't have to re-type complicated PVS formulas. File and index mode are nice when you have a family of theories and need to describe them all.

Downloads
The LPP There is more extensive documentation and examples in the comments at the top of the LPP. BSD License.
The style file The style-file is relatively undocumented. I'm working on improving that. BSD License.

Last changed Mon Nov 1 16:14:47 MET 2004