[Tlaplus-users] First impressions using TLAPS
Leslie Lamport
lamport at microsoft.com
Lun 31 Mai 17:09:22 CEST 2010
Hi Matthieu,
Stephan has answered most of your questions; I'll just fill in some details. But first, the Toolbox interface to TLAPS is almost ready and will be in the next Toolbox release--I hope in a few weeks. Most of your observations will be obsolete (except, we hope, for how nice TLAPS and the proof language are).
> 2. When the module does not have the same name than the file (e.g.
> MODULE SpinLocke in SpinLock.tla), the parser fails with that error:
> error:
The spec must be checked for errors by SANY, the regular TLA+ parser, before being run through TLAPS--otherwise, the proofs may be unsound. This is done automatically by the Toolbox. SANY produces a much friendlier error message, and clicking on it in the Toolbox takes you to the right place in the module to correct it.
I am not sure I completely understand. Do you mean you stated two theorems (with their proofs)
in your module that asserted the same statement? TLAPS would not be clever enough to detect
this. Or just one THEOREM followed by two proofs?
Stephan underestimate's TLAPS's cleverness. If you ask TLAPS to prove something that is syntactically identical to a known fact, it reports that it is trivially true.
> 4. When there are no proof for a theorem, the system does not
> complain. This is interesting when writing proofs incrementally,
> (because some steps may be omitted), but I think it would be
> interesting to have an option that checks that there exists a proof
> for every theorem (I've been wondering for some time why a proof
> worked because I forgot to write a proof for a QED). Maybe I did
> not see it?
I think the --status option causes tlapm to report the locations of all missing or OMITTED proofs. The Toolbox will indicate by shading which steps have incomplete (sub)proofs.
Thanks for your comments (and compliments). I hope you'll start using the Toolbox even before the next version is released. (If you do and send us your comments, the next version just might fix any problems you find.) I can't overemphasize the virtues of using the model checker to find errors before trying to prove something. Even if your system is too big to be model checked on any but the tiniest models, even checking those tiny models will quickly catch stupid errors that could lead to a lot of wasted time when writing a proof. Remember this very important observation:
It's a lot easier to prove something if it's true.
For another example of using the model checker, download my paper "Implementing Dataflow With Threads" from
http://research.microsoft.com/apps/pubs/default.aspx?id=64625
Look at Section 3.1.2 (pages 8-9), which asserts four facts. I never proved those facts. Instead, I used the TLC model checker to test that they were correct for large enough ranges of values that I was convinced that they were right. This gave me more confidence in their correctness than any hand proof would have. Now that I have TLAPS, I could have proved them formally to get even more confidence. But I still would have checked them first with TLC, because I know that it's a lot easier to prove something if it's true.
I actually wouldn't bother proving those facts because I'm interested in proving the correctness of systems, not in proving mathematical theorems. Given all the possible sources of error in a system--even if a mathematical model of the system has been proved correct--and the amount of time one has to check the system, it is likely to be a waste of time to prove anything for which model checking can give you a high degree of confidence in its correctness. I consider it a major advantage of using TLAPS that you can apply a prover and a model checker to specs written in the same language, and you can use whichever is most appropriate for any particular task.
Leslie
More information about the Tlaplus-users
mailing list