Examples of specs with proofs that use subexpressions?

[Andrew Helwer]

Been reading the TLA+2 language spec and had no idea that subexpressions existed and were so powerful. You can use the language itself to navigate around the parse tree of the TLA+ file you're working in! Are there any examples of TLAPS proofs which use this? Also, does TLC support it (although I assume it's quite inefficient)?

Andrew

[Karolis Petrauskas]

Do you mean such an example?

https://github.com/tlaplus/DrTLAPlus/blob/master/Paxos/Paxos.tla

Don't know if that works in TLC.

Karolis

On Mon, Apr 26, 2021 at 9:03 PM Andrew Helwer <andrew...@gmail.com> wrote:

Been reading the TLA+2 language spec and had no idea that subexpressions existed and were so powerful. You can use the language itself to navigate around the parse tree of the TLA+ file you're working in! Are there any examples of TLAPS proofs which use this? Also, does TLC support it (although I assume it's quite inefficient)?

Andrew

--
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/21cd1584-64a0-469e-bdb5-ddd8fd8d19dbn%40googlegroups.com.

[Andrew Helwer]

Hi Karolis,

By subexpressions I mean stuff like foo(2, 3)!bar!<<!(1)!:!>>, which you can use to refer to specific parts of a larger expression. The linked proof does use subexpressions in a limited way, to bind quantifiers, but not in a more involved way.

Andrew

[Karolis Petrauskas]

I tried to use sub-expressions in proofs (in a similar way, as in the Paxos proof), but for me it looks like it should be quite fragile, if paths would become longer than a few levels.

It becomes not obvious how to fix a broken path to a sub-expression after the spec itself is modified. Often it is hard to guess, which expression was referred before the modification of the spec.

And they are actually hard to read, again, if they are longer than a few levels. You need to jump between the proof and the formula itself.

But that's just my impression.

Karolis

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/88d70b38-4c59-4134-9112-fb993521923fn%40googlegroups.com.