[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

Re: pluscal overhead



Thank you Leslie and Stephan, really appreciate your insights!

On Sunday, May 3, 2015 at 1:13:22 PM UTC-7, Leslie Lamport wrote:

Hi Yuri,

There are two good reasons to use PlusCal instead of TLA+.

1. Most people who don't know TLA+ find PlusCal easier to understand.
This can make a big difference if you're writing something to be read
by others.  That's why I've published several algorithms in PlusCal
but I don't remember publishing one written in TLA+.

2.  Traditional multiprocess synchronization algorithms involve
control state.  I usually find it more natural to describe that
control state using PlusCal's programming-language structures rather
than explicitly introducing the pc variable.  (This applies as well to
sequential programs.)

Related to 1 is the fact that you can write f[x] := e instead of the
uglier

   f' = [f EXCEPT ![x] = e]

I believe that most uses of procedures are not the best way to express
the desired algorithm.  As Stephan suggested, if a procedure has only
a single label at the beginning, then it is almost always better to
either replace it with a macro or else define a TLA+ operator that
allows you to replace the procedure call with a simple assignment
statement.  People who are not used to programming with functional
languages often don't understand how anything computed with a loop
can easily be computed by a recursively defined TLA+ operator.

Leslie