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

*From*: c.burge.glasgow@xxxxxxxxx*Date*: Thu, 16 Apr 2020 10:19:31 -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>

Hi again!

But I am not at all confident that I'm right!

On Wednesday, April 15, 2020 at 5:19:02 PM UTC+1, Stephan Merz wrote:

-- I've been looking at the TLAPS tutorial, but I'm afraid it still doesn't quite make sense to me.

I've gone for:

THEOREM diagseq == Spec => [](diag = tdiag)

ASSUME Init == (diag = tdiag)

THEOREM Next (diag = tdiag) /\ [Next]_vars => (diag = tdiag)'

Init QED BY Init, Next, PTL DEF Spec

PROOF BY DEF Spec, Init

On Wednesday, April 15, 2020 at 5:19:02 PM UTC+1, Stephan Merz wrote:

The reason the formula only talks about the initial state is that it does not contain any temporal operator. If you want to prove that it holds for all states, you should writeTHEOREM Spec => [](diag = tdiag)This is an invariant, and from a quick glance at the algorithm it appears that it is inductive. You can prove it as follows:<1>1. Init => (diag = tdiag)<1>2. (diag = tdiag) /\ [Next]_vars => (diag = tdiag)'<1>. QED BY <1>1, <1>2, PTL DEF Spec(You'll have to write proofs for the steps <1>1 and <1>2 in order to complete the proof.) If this doesn't make sense to you, please have a look at the TLAPS tutorial [1].Stephan[1] http://proofs.tlapl.us/doc/web/content/Documentation/ Tutorial/The_example.html On 15 Apr 2020, at 18:10, christi...@xxxxxxxxx wrote:Another quick question:I can see that my assertion only talks about the initial state (I'm guessing that's what the 'Init', in "BY DEF Spec, Init" does.)Is there a reason why that would not be sufficient proof for my spec? Do you mean that it's just comparing two empty lists?

On Wednesday, April 15, 2020 at 4:11:06 PM UTC+1, Stephan Merz wrote:1. Your algorithm is written in PlusCal, which appears as a comment to TLA+. You first need to generate the TLA+ specification (File -> Translate PlusCal Algorithm in the Toolbox).2. Your theorem should then be stated as a consequence of the specification in the formTHEOREM diagseq == Spec => (diag = tdiag)Its proof will look like "BY DEF Spec, Init". Note that your assertion only talks about the initial state.Regards,StephanOn 15 Apr 2020, at 17:04, christi...@xxxxxxxxx wrote:Hi!I've written a specification to transpose a matrix, but I don't know how I use TLAPS to prove correctness. I've tried:

---- MODULE transp ----EXTENDS Naturals, TLCCONSTANT n, m(* --algorithm transposevariables i=1, j=1, array = <<<<>>,<<>>>>,transp = <<<<>>,<<>>>>, diag = <<>>, tdiag = <<>>,beginwhile j <= m doi := 1;while i <= n dotransp[i][j]:= array[j][i];if i = j thendiag[j]:=array[j][i];tdiag[j]:=transp[i][j];end if;i := i+1;end while;j := j+1;end while;print array;print transp;end algorithm *)THEOREM diagseq == diag=tdiagPROOFOBVIOUSBut I get the error that tdiag is unknown. I'm not sure what I'm not understanding so any help would be appreciated!--

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 tla...@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a70545cd-37a0- .430a-aad5-bc303a0f33e0% 40googlegroups.com

--

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 tla...@googlegroups.com .

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01d5937b-63df- .4723-96c7-14153a75b529% 40googlegroups.com

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/261f1d34-d328-4028-91f4-7c172a6be0c2%40googlegroups.com.

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

**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

- Prev by Date:
**Re: [tlaplus] How do you list possible next steps?** - Next by Date:
**Re: [tlaplus] Proving a Matrix Transpose** - Previous by thread:
**Re: [tlaplus] Proving a Matrix Transpose** - Next by thread:
**Re: [tlaplus] Proving a Matrix Transpose** - Index(es):