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

*From*: christina.a.burge@xxxxxxxxx*Date*: Wed, 15 Apr 2020 09:10:30 -0700 (PDT)*References*: <a70545cd-37a0-430a-aad5-bc303a0f33e0@googlegroups.com> <3F9142EF-641E-4A04-8650-DFE1CAC46592@gmail.com>

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:

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

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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01d5937b-63df-4723-96c7-14153a75b529%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

- Prev by Date:
**Re: [tlaplus] Proving a Matrix Transpose** - 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):