[Tlaplus-users] First impressions using TLAPS
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:
File "./SpinLock.tla", line 1, character 17
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