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

Re: [PVS] Semi-literate specification with PVS



-----BEGIN PGP SIGNED MESSAGE-----
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 
up.

> 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.
#
# %+IGNORE
# %+RESUME
#   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.

[ade]

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 
somewhere.


-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.2.4 (FreeBSD)

iD8DBQFBK6YpdqzuAf6io/4RAiI/AKCQUrOsaMy6F9Yk3MBQDEo8D+/O/wCbBdWg
/kI2QIDP4+T5Vs/9RCP4o5c=
=UF6N
-----END PGP SIGNATURE-----