How to verify a parser in TLA+?

[Delta Striker]

I'd like to verify a LL(1)-style parser using formal verification.

But I don't have any idea how to model the specification of the parser.

Are there any examples about this,or can you give me some hint?

Thank you.

[Stephan Merz]

I am not aware of work on parser verification performed in TLA+. The Menhir parser generator [1] for OCaml, based on LR(1) rules, includes a Coq backend for formal verification (section 12 of the reference manual), but I have never used this functionality. Perhaps you can get some inspiration there.

Regards,

Stephan

[1] http://gallium.inria.fr/~fpottier/menhir/

--
You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b2b5601d-19c4-4c0d-9f5b-17a6a0def3e2n%40googlegroups.com.

[Andrew Helwer]

It's hard to say what a formal spec for a parser would even look like, other than an EBNF grammar, but there are tons of very solid battle-tested parser generators that will happily take an EBNF grammar and create a full parser for you.

Andrew