Re: Availability of foundation modules with SciPy and NumPy capability

[Ian Wilkinson <ian.wi...@xxxxxxxx>]

Hi Leslie,

Disaster! Defeated in the second paragraph.

Yes, we would be employing real numbers. Apologies,
we should have given greater care on consideration
and discovery on TLA+ support for this.

Conceptually, it sounded a fine approach for us.

Hugely grateful for insight,
ian


On Tuesday, May 5, 2015 at 11:12:17 AM UTC+1, Leslie Lamport wrote:
> Hi Ian,
> The answer to your question depends on what you want to do with the
> specifications you write.  My guess is that you want to write
> algorithms in TLA+/PlusCal, debug the algorithms using the TLC model
> checker (or possibly by writing proofs of correctness that you check
> with the TLAPS proof system), and then implement those algorithms in
> programs (probably in Python with SciPy and NumPy).  If this guess is
> incorrect, please stop reading now and tell us what you do want to do
> with the specifications.
> If you're still reading, the answer depends on whether your algorithms
> manipulate real numbers (presumably implemented in the programs with
> floating-point arithmetic).  If they do, then TLA+ is probably not for
> you because TLC does not do arithmetic with real numbers.  (If you
> only want to write proofs the answer is probably the same because
> TLAPS does not have good facilities to handle real arithmetic, but
> it's not completely out of the question.)
> If you've gotten this far, then your algorithms use only integer
> arithmetic and things look promising.  So, we come to your question
> about SciPy and NumPy, about which I know nothing.  Wikipedia tells me
> that NumPy provides an efficient implementation of dynamic
> multi-dimensional arrays.  TLA+ (and hence PlusCal) handles "dynamic
> multi-dimensional arrays" (which are simply what mathematicians call
> functions over a Cartesian product).  However, it does not provide
> "efficient implementation".  Model checking effectively does
> exhaustive testing of a small model of the algorithm--for example,
> over all arrays with a very small dimension and a small number of
> elements.  How big "small" is depends on the application.
> As for SciPy, it seems to be a mixed bag.  Probably none of the things
> it offers are already built into TLA+.  Some things are obviously not
> something TLA+ is good for--like plotting.  Anything that involves
> mathematical computations can in principle be written in TLA+.
> Anything that can be described by a mathematical function is probably
> easy to write in a few lines of TLA+.  Other things, like symbolic
> math, might be too much work to be worth the effort.  Again, don't
> expect efficiency.
> Leslie