Re: Proofs of integer properties

Hi again,

Yes I am reading through the hyperbook. I am working through Euclid's algorithm (PlusCal) right now, I am having some trouble:

1) GCD3 theorem information in the text seems to suggest the following should work:
==========================
THEOREM GCD3 == \A m, n \in Number : (n > m) => (GCD(m, n) = GCD(m, n-m))
<1> SUFFICES ASSUME NEW m \in Number, NEW n \in Number,
                      n > m
               PROVE GCD(m, n) = GCD(m, n-m)
    OBVIOUS
<1>1. \A i \in Int : Divides(i, m) /\ Divides(i, n)
                      <=> Divides(i, m) /\ Divides(i, n - m)
    BY LemmaDiv DEF Divides
<1> QED
    BY DEF GCD, SetMax, DivisorsOf, Divides
==========================
But <1>1 doesn't prove. I probably misunderstood.

2) The proofs section breaking down Inv /\ [Next]_vars => Inv', I needed to add 'BY UNCHANGED vars' to steps <2>2 and <2>3. It didn't seem to pick it up from ASSUMES, and I didn't see anything in the text about it.

3) I couldn't get a TLC model to run with the Euclid PlusCal module. It just won't start, no error messages or anything. I had a model running for GCD module just fine.

4) I saw an assertion when I accidentally put a proof step <1>4 in USE DEF <1>4 instead of USE <1>4 DEF .. I assumed it was not surprising this caused weirdness.

In general I am really impressed with the quality of the environment and the documentation. I have wanted to look into using formal methods for a while but the literature is almost incomprehensible. You really need to just dive in and play with it, but then the trick is finding tools etc. etc. For learning purposes it really helps to just be able to jump in, build a specification, test it against a model and then prove it.

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.

Regards,
Chris.