[Tlaplus-users] First impressions using TLAPS

Matthieu Lemerre matthieu.lemerre at cea.fr
Lun 31 Mai 16:22:25 CEST 2010


I've been trying TLAPS on a small example (proof of critical section
using a Compare-and-swap based spinlock) and things go well so far.
Proving type invariants was trivial, and I'm half-way proving the
"interesting" invariants. The proof language is natural and easy, the
tools avoid entering into too much details (e.g. the proof of type
invariant only takes 5 lines) and I believed that writing formal proof
would have been much harder, so thanks!

Anyway I wanted to share some initial thoughts and minor nitpicks I
found (before I get used to the system :)). I hope that this will be
useful to you.

1. Tabs are no longer allowed in TLA+, but pressing tab kept inserting
   them (even if they were displayed in red). The following trivial
   patch makes so that pressing the Tab key directly insert spaces
   instead of tabs.

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:

make proof
../tools/tlaps-0.9.2010_04_06_03/bin/tlapm SpinLock.tla
File "./SpinLock.tla", line 1, character 17
[Internal] <?>
File "<unknown>":
Error: Could not parse "./SpinLock.tla" successfully.
 Tlapm ending abnormally with Failure("Module.Parser.parse_file")
make: *** [proof] Error 1

3. (Maybe normal) I tried to prouve the same theorem using two
   different proofs, the first proof was normal, and the second proof
   was incomplete. When I commented out the first proof, the system
   rightly complained, but not when it was present. I think this
   behaviour might be surprising.

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?

These problems are all very minor once we are aware of their presence,
but may be surprising at first.


More information about the Tlaplus-users mailing list