"How to Write a Long Formula"

Dave Long dl@silcom.com
Wed, 24 Apr 2002 11:39:10 -0700


In Lamport's "How to Write a Long Formula" (SRC119)
he proposes an indendation based notation, in which
associative operators can be written redundantly to
avoid parentheses and provide context.

-Dave

Instead of:

	&& (for all c in CacheAddress:
		cache[p,c] in ([adr:Address,val:Value]+{"Invalid"}),
	   || (request[p] in Request,
              && (request[p] == "Ready",
                 state[p] == "Idle")),
	   response[p] in Value)

by rewriting associative formulae (A&&B&&...&&Z) as
	&& A
	&& B
	...
	&& Z

he suggests:
	&& for all c in CacheAddress:
		cache[p,c] in ([adr:Address,val:Value]+{"Invalid"}),
	&& || request[p] in Request
	   || && request[p] == "Ready"
	      && state[p] == "Idle"
        && response[p] in Value