[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: Christina Burge <christina.a.burge@xxxxxxxxx>*Date*: Fri, 17 Apr 2020 09:43:14 -0700 (PDT)*References*: <a70545cd-37a0-430a-aad5-bc303a0f33e0@googlegroups.com> <3F9142EF-641E-4A04-8650-DFE1CAC46592@gmail.com> <01d5937b-63df-4723-96c7-14153a75b529@googlegroups.com> <730D2F51-FD92-4F40-BB2E-57E5CE211791@gmail.com> <261f1d34-d328-4028-91f4-7c172a6be0c2@googlegroups.com> <C4A35F91-8086-4398-B6CE-DCC1EFE4B63D@gmail.com>

Thanks for your help! As you can probably tell, I am very new at this and has missed that my algorithm is not working as intended, so thanks for the fix.

-- I am currently combing through the hierarchical proofs section of the tutorial. hopefully I will find it illuminating!

On Friday, April 17, 2020 at 8:56:59 AM UTC+1, Stephan Merz wrote:

On Friday, April 17, 2020 at 8:56:59 AM UTC+1, Stephan Merz wrote:

Hello,first of all, looking back at your algorithm it seems to me that you did not write what you intended to. In particular, all matrices and vectors were initialized to empty sequences and then updated using EXCEPT. In TLA+,[f EXCEPT ![x] = y] = [z \in DOMAIN f |-> IF z=x THEN y ELSE f[z]]As you can see, the domain of the function (or sequence) does not change in the update, and so all your matrices and vectors are still empty at the end. Although this does not invalidate your property, it is certainly not what you meant.Second, `array' is really an input of the algorithm. I made it a parameter of the specification so that one can try different inputs using TLC. And it is clear that the parameters n and m should be the dimensions of the input matrix. Moreover, the way the algorithm is written makes sense only if n <= m so that we don't get out-of-bound accesses to the matrix.All of this could have been revealed by running TLC over a few instances of your algorithm. Before you embark on a proof, it is good practice to check your specification using TLC as thoroughly as you can so that you are confident that your theorem is actually true.Turning to the proof, I have to step back from what I said before: your correctness property is indeed inductive, but only modulo type correctness of the algorithm. I therefore stated (and model checked, but did not prove) a type correctness theorem and used it to prove your correctness property. The result is in the attached TLA+ module. Proving the typing invariant is left as an exercise, which should not be difficult.The proof that you copied into your post is not even syntactically correct. I hope you will understand proofs better by looking at the proof in the module and at the TLAPS tutorial.Regards,Stephan

You received this message because you are subscribed to the Google Groups "tlaplus" group.

To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/784e3b75-f333-42e7-ace1-1bcdef0381ea%40googlegroups.com.

**References**:**[tlaplus] Proving a Matrix Transpose***From:*christina . a . burge

**Re: [tlaplus] Proving a Matrix Transpose***From:*Stephan Merz

**Re: [tlaplus] Proving a Matrix Transpose***From:*christina . a . burge

**Re: [tlaplus] Proving a Matrix Transpose***From:*Stephan Merz

**Re: [tlaplus] Proving a Matrix Transpose***From:*c . burge . glasgow

**Re: [tlaplus] Proving a Matrix Transpose***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Proving a Matrix Transpose** - Next by Date:
**Re: [tlaplus] How do you list possible next steps?** - Previous by thread:
**Re: [tlaplus] Proving a Matrix Transpose** - Next by thread:
**[tlaplus] TLAPS: problem with proof of GCD from TLA+ Hyperbook (chapter 11.2)** - Index(es):