[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
[PVS-Help] Re: PVS Grammar in BNF
On 19 May 2005, at 16:59, Nathaniel Ayewah wrote:
> Hi Joe,
> Thanks for the response. We are trying to extract the components of
> theories written in PVS to verify a microprocessor -- the aim is to
> effectively visualize the theories and make them more accessible. In
> particularly, we want to be able to automatically create schematic
> diagrams for the parts of the theories that represent structural
That is a very cool idea/project. Is the a particular (perhaps
domain-specific) representation you wish to use for such?
> I have created a parser that seems to be able to parse many of the
> we are working with (this is after much sweat and tears). Are there
> existing parsers that we could use?
The one built into PVS? :)
Seriously, you should consider such, if you are willing to live in
PVS and emit these kinds of visualisations. This means basically
writing a visitor in Lisp to walk over the internal (typechecked)
representation, pulling out the bits you need. I plan on doing this
kind of thing for my next project as well, so perhaps it is just time
for us to add a real visitor framework to PVS and do it once,
correctly, in a well-documented way, for good.
This perspective is based upon my past experience: I have also build
a PVS parser that (after very much blood, sweat, and tears) parses
nearly all of the PVS I have. Unfortunately, I do not think you'll
be interested in it as it is written in Emacs lisp using the wisent
framework from more than a year ago and thus needs to be updated.
Department of Computer Science
University College Dublin