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

[PVS-Help] RE: PVS Grammar in BNF

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

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?


Nathaniel Ayewah
Computer Science, Southern Methodist University
Dallas, TX, USA

-----Original Message-----
From: Joseph Kiniry [mailto:kiniry@acm.org] 
Sent: Thursday, May 19, 2005 4:46 PM
To: nat@natidea.com
Cc: pvs-help@csl.sri.com
Subject: Re: PVS Grammar in BNF

Hi Nat,

On 19 May 2005, at 11:09, Nathaniel Ayewah wrote:

> Is there a plain Backus-Naur Form (not extended bnf) grammar for PVS? 
> I've tried converting the extended grammar to bnf and compiling the 
> grammar with a LALR parser and had many shift-reduce conflicts.
> For example, when parsing a TheoryDecl, how can the parser
> differentiate
> between a list of Ids (as in TypeDecl) and a list of IdOps (as in
> VarDecl)?

The PVS grammar is the most context-sensitive grammar I have ever  
tried to parse.  I think that you will find that, even once you  
introduce quite a bit of type and expression context to your LALR  
parser, you will still see lots of conflicts.  Parsing PVS outside of  
PVS is not for the faint-hearted.  May I ask what your needs are wrt  
parsing PVS?

Joseph Kiniry
Department of Computer Science
University College Dublin