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

[tlaplus] Re: Is TLA spec shorter than code?

You should not expect a TLA+ specification of a program to be shorter
than the program.  Programming languages are designed to write
programs.  There's no reason a TLA+ spec that captures the meaning of
a program should  be as short as the program itself.  For example, the
program might have an assignment statement x = x+1 .  The TLA+ formula
x' = x+1 may look similar, but it's not at all the same.  For one
thing, the statement x = x+1 is supposed to throw an exception if x
is too large.  So, its TLA+ representation would have to be something

  IF x+1 =< MaxInt THEN x' = x+1 ELSE ...

plus a whole lot of additional math representing the actions that
describe exception handling.  On the other hand, how would you express
the TLA+ formula x' = x+1 in the programming language?  Program code
to add two arbitrary integers is not going to be simple.  (Of
course it won't be difficult if someone has aleady implemented it; but
a TLA+ spec that someone has already written isn't hard to import

Programming languages make it easy to handle the complexities of
arithmetic on a finite set of integers, and hard to do simple
arithmetic on the actual set of integers.  It's obvious why
programming language designers made that choice.  It's less obvious
why I made the opposite choice for TLA+, and most people don't
understand it.  To get a hint of the reason why TLA+ is so different
from programming languages, read the story of the OpenComRTOS project 
described here:


Experienced programmers don't get a factor of 10 reduction in code
size by improving their programming; they do it by changing the way
they think.  Learning to think in terms of algorithms and high-level
concepts rather than programs and code takes time and practice.  I
learned to do it before I became a computer scientist, but it took me
25 years to figure out how to embody that kind of thinking in a
specification language.  Don't expect to learn it in a few days.


You received this message because you are subscribed to the Google Groups "tlaplus" group.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To post to this group, send email to tlaplus@xxxxxxxxxxxxxxxx.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/2ca04342-768f-47b8-9448-5d3f42cea343%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.