[Tlaplus-users] Seemingly circular proofs

Maniatis, Petros petros.maniatis at intel.com
Mer 7 Juil 03:25:36 CEST 2010


Hi all,

 

I've been looking at the consensus example in the tlaps release, trying to
understand more complex proofs for more complex systems. I've encountered a
few SUFFICES steps whose proofs seem to be pointing to the SUFFICES step
itself. For example, in voting, the <1>1 step of the ShowsSafety theorem
reads

 

<1>1. SUFFICES ASSUME...

               PROVE ...

  BY <1>1 DEF ...

 

Is this shorthand for USE DEF ...  followed by OBVIOUS?

 

BTW, is there, by any chance, an annotated (explained or commented) version
of the consensus spec and proof? It is a rather daunting example, but a good
advanced example, so any help in understanding why the proof is the way it
is would be very very helpful. Especially helpful would be some explanation
of the set theorems in the associated module.

 

Thanks!

 

Petros

 

------
Petros Maniatis

Research Scientist
Intel Labs Berkeley 

 

-------------- section suivante --------------
Une pièce jointe HTML a été nettoyée...
URL: <http://lists.gforge.inria.fr/pipermail/tlaplus-users/attachments/20100706/aa34ba30/attachment-0001.htm>
-------------- section suivante --------------
Une pièce jointe autre que texte a été nettoyée...
Nom: smime.p7s
Type: application/x-pkcs7-signature
Taille: 7151 octets
Desc: non disponible
URL: <http://lists.gforge.inria.fr/pipermail/tlaplus-users/attachments/20100706/aa34ba30/attachment-0001.bin>


More information about the Tlaplus-users mailing list