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

*From*: Leslie Lamport <tlapl...@xxxxxxxxx>*Date*: Tue, 5 May 2015 03:12:17 -0700 (PDT)*References*: <9323db0d-63f1-49f8-9c10-f880113eacc9@googlegroups.com>

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

**Follow-Ups**:**Re: Availability of foundation modules with SciPy and NumPy capability***From:*Ian Wilkinson

**References**:**Availability of foundation modules with SciPy and NumPy capability***From:*ian . wi . . .

- Prev by Date:
**Availability of foundation modules with SciPy and NumPy capability** - Next by Date:
**Re: Availability of foundation modules with SciPy and NumPy capability** - Previous by thread:
**Availability of foundation modules with SciPy and NumPy capability** - Next by thread:
**Re: Availability of foundation modules with SciPy and NumPy capability** - Index(es):