[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
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  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.
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?
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+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ef88adbd-a7d0-4979-8671-0562a797a82cn%40googlegroups.com.