Re: Proofs of integer properties

On Monday, November 10, 2014 11:23:50 AM UTC-8, Leslie Lamport wrote:

   One comment about the hyperbook in particular, the text description building up proofs is good to follow along and
   force you to think but when there is a problem it's easy to get lost without reference to the final working TLA+ text.

   It might be helpful to have the actual TLA+ modules accompany the hyperbook, rather than just the PDF versions (even the ASCII in PDF form).

   Agreed.

In general, I have tried to present a complete module after developing it bit by bit. However, sometimes a module isn't developed bit by bit, but a first version is developed, then it is modified to form another version, then modified again and again. So, instead of having a single complete module, there are quite a few. In those cases, it seems impractical to provide a complete module for each of those versions. Perhaps someone has a suggestion on what to do in that case. However, it is possible that there are places where it would be reasonable to provide a complete module (or perhaps a complete proof) and I have failed to do so. I would appreciate having those exact places pointed out.

Thanks,

Leslie

The specific proof I got stuck on was the full proof (proof track) of Euclid's algorithm, where you decompose Inv /\ [Next]_vars.

First I got stuck for a while getting it to decompose the same way as you described, then after I got the decomposed proof stages to match I hit the above problems trying to prove.

This proof is quite useful because it is the first proof I saw that walks through the full process generating a specification using PlusCal to full proof. For that reason I think it is worth including the final text of this proof.

It wouldn't hurt to have a repository of examples linked directly off the website, rather than including all examples with the book. I keep losing track where I found various interesting proofs, in TLAPS examples, papers or one of the books. For certain proofs like Euclid's algorithm it is valuable to have several proofs that take different approaches to contrast.