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

[PVS-Help] Re: PVS Grammar in BNF

Hi Nat,

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

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  
> files
> we are working with (this is after much sweat and tears). Are there  
> any
> 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.

Joseph Kiniry
Department of Computer Science
University College Dublin