[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
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
Can I create a type that maps to multiple types?
Thanks in advance,