[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: [PVS] Semi-literate specification with PVS

Hash: SHA1

On Tuesday 24 August 2004 16:29, Pertti Kellomäki wrote:
> It has been pretty quiet on the list, so I thought I'd share a

Indeed it has - quite unfortunate, really. I'm working up a bunch of stuff 
based on some ACL2 tutorials I recently attended - basically a bunch of 
"things PVS should do better" proposals, possibly with some code to back them 

> little bit of Python that I am using for semi-literate specification
> with PVS. It takes a LaTeX file produced by PVS, and chops
> it up at lines that match fragmentBoundaryRe. The resulting
> fragments are stored in a directory whose name is the name
> of the LaTeX file sans the ".tex" extension. One can then use
> the fragments to build a fancy LaTeX document out of the
> specification.

Hm, interesting, that's a lot like the literate PVS I've been using for a few 
years; instead of using PVS's LaTeX output (which I find rather ugly and 
clumsy) , I use various kinds of comments to direct a perl program that reads 
the PVS file that outputs one or more LaTeX files based on the PVS. From the 
docs of that particular tool: (LPP stands for Literate PVS Processor)

# 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:
# * Six percent signs (yes, %%%%%%) are meta-comments and are deleted
#   from the output in all processing modes. I Typically use these
#   comments for the copyright header at the top of the file and to
#   set off blocks of PVS code from each other.
# * Three percent signs (%%%) are output as regular text in the file
#   mode. The text after the percent signs can contain whatever LaTeX
#   commands you like -- it's output as-is. In block mode, three percent
#   sign comments are deleted from the output.
# * One percent sign (%) is output as regular text in block mode and deleted
#   in file mode.
# In addition, comments that start with %+ are processing instructions for
# the LPP.

# LPP commands for block and file mode.
# %+BEGIN <blockname>
# %+END <blockname>
#   These two comments control the LPP in block mode. In block mode, all
#   PVS code between the BEGIN and END is written to a _separate_ LaTeX
#   file named pvs-<blockname>.tex. If you use the same <blockname> more
#   than once in a PVS file, all the blocks are written together to the
#   output file. This lets you (re)group your PVS code to reflect your
#   presentation instead of the order it is in the PVS file in.
#   These comments direct the LPP in file mode. All text between the
#   IGNORE and RESUME is ignored, and not printed to the output file.
#   If index mode is on, then LEMMA and INDEX entries _are_ indexed
#   even in IGNORE blocks. (For index mode, see below)
# You can mix and match BEGIN/END and IGNORE/RESUME blocks however
# you wish, because the comments apply to different modes of running
# the LPP.

I find that it is rarely useful to embed too much documentation about the PVS 
in the comments - if I'm going to describe some theory at length I'll do it 
in a separate article where I'd like to be able to include lots of fragments 
of PVS code. The block-mode comments are very useful for that - put a 
%+BEGIN / %+END pair around a fragment that you'd like to refer to and then 
\input the resulting LaTeX file.


PS. The source of the tool is about 14k (I write pretty verbosely commented 
perl), hence I'm not attaching it; if there's any other interest I'll post it 

Version: GnuPG v1.2.4 (FreeBSD)