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

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

Thanks Stephen! I should have said that I'd already translated it, I didn't include the translation for brevity (always a mistake, when will I learn?).

-- I'll try moving my theorem to the end of the TLA+ translation, thanks!

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/d6a90862-d6dd-43b6-9783-8199292f21e4%40googlegroups.com.

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

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