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

Re: Availability of foundation modules with SciPy and NumPy capability

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,

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