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

[PVS-Help] Help with Testing HTML Renderer


I was interested in learning to use PVS and was going to input the HTML BNF grammar and related specs
into it to prove that there is not enough information to completely specify some layouts.
I might be creating something more complicated than I realize but it's something I'm interested at the moment.

I've gone through the tutorials and looked at the guides but I'm stuck on how to input the BNF grammar.
For example the BNF grammar for HTML shows:

a_content ::= heading | text

so can I do the following in PVS

  Link: TYPE
  Text: TYPE
  Heading: TYPE
  A_Content: TYPE = (Heading OR Text)

a_tag: [a_content: A_Content, link: Link]

It parses okay but I'm not sure PVS and I are thinking the same way about it.
Can I create a type that maps to multiple types?

Thanks in advance,

Phillip Soltan
email: phillipsoltan@xxxxxxxxx