Re: [tlaplus] How to verify a parser in TLA+?

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.

On Wednesday, January 11, 2023 at 5:28:05 AM UTC-5 Stephan Merz wrote:

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/

On 10 Jan 2023, at 08:06, Delta Striker <unicorn8...@xxxxxxxxx> wrote:

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.

--
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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/b2b5601d-19c4-4c0d-9f5b-17a6a0def3e2n%40googlegroups.com.