"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