Re: Pcal, procedures and tests

[Leslie Lamport <tlapl...@xxxxxxxxx>]

Hi Frederic,

   The only downside is that TLC favors algorithms over CHOICE or even
   recursion.  But it deserves to be tried.

   A solution might be to have a library of boosted specifications.  For
   example a specification of a sorting algorithm but with a piece of
   code behind to speed up TLC.

The only good reason to write a library module to aid model checking
is to define operators that TLC can't handle (except perhaps at
exorbitant computation cost) without overriding the definition with
Java code.  For example, it seems to be impossible to define Seq so
that TLC can evaluate the _expression_ seq \in Seq(Nat) when seq is a
sequence.  For example, there was no need for the standard Bags
module.

The problem of writing a sorting operator that TLC can evaluate
efficiently is discussed in Section 9.2 of the Hyperbook.  The
definition given there is five lines long.  The time-complexity of
that algorithm is O(n^2).  If you need a more efficient algorithm, you
could find one in an algorithm book somewhere and code it as a
recursively defined TLA+ operator.  But if O(n^2) isn't good enough,
you are probably using TLA+ to do things it wasn't meant to do.

One of the differences between programming and specification is that
re-use is not an issue.  If you want to re-use something you've
defined elsewhere, copy-and-paste is good enough.  (Imagine what
programming would be like if no one wrote programs longer
than 2000 lines.)  The operator defined in the Hyperbook sorts a set
of records according to a 'key' field, because that's what was needed
in the example of Section 9.  If this was programming, I'd have
written a sorting procedure to handle any sorting task, involving
callbacks to compute the sorting keys.  But there's no need for that
for a definition I can write in 5 lines.  If I needed to sort a
sequence of integers, I could just copy the definition from the
HyperBook and modify it in a straightforward way.

Leslie