Re: RECURSIVE as a forward declaration

Thanks.

I actually have two "sections", one dealing with messaging and one with operations (it's a distributed data store), and I'd rather keep the definitions grouped. Some messaging actions retry operations, and operations result in messages sent. I'm not planning on using TLAPS (only TLC), so I'll help myself to some judicious use of RECURSIVE, then.

Thanks for the tip about name links working in comments! That'll come in handy.

On Wednesday, October 14, 2015 at 11:02:26 AM UTC+3, Leslie Lamport wrote:

The only bad effects of using RECURSIVE to write definitions out of
order are that it will confuse readers of the spec and will make it
impossible to use TLAPS to check proofs of properties of the spec.

I presume you want to do things like define the next-state action in
terms of its sub-actions before defining those sub-actions. A better
idea is to explain in a comment the purpose of those sub-action
definitions. The reader can jump from a name to its definition (by
Control+Left-click on the name or by placing the cursor on it and
typing F3) even if the name appears in a comment.

Leslie

On Tuesday, October 13, 2015 at 9:55:22 PM UTC-7, Ron Pressler wrote:
Hi!
I'm new to TLA+, and so far I love it! I've begun using it to specify a distributed data store.

So far I have one small issue (and a few bigger ones, which will require another post): the requirement for all definitions to be defined before their use may impose a less-than-ideal organization on the spec, which might harm its readability. My question is, is it safe/idiomatic to use the RECURSIVE declaration as a forward declaration in the general case (i.e. not for operators that are actually recursive, nor immediately preceding the definition)?

Ron