[PVS-Help] Help with Testing HTML Renderer

[Phillip Soltan <phillipsoltan@xxxxxxxxx>]

Hello,

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