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

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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

--
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/4546591B-0CE4-44F5-B57C-6A377E6148F7%40gmail.com.