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

*From*: christina.a.burge@xxxxxxxxx*Date*: Wed, 15 Apr 2020 08:04:53 -0700 (PDT)

Hi!

But I get the error that tdiag is unknown. I'm not sure what I'm not understanding so any help would be appreciated!

-- 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 do i := 1; while i <= n do transp[i][j]:= array[j][i]; if i = j then diag[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=tdiagPROOFOBVIOUS

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/a70545cd-37a0-430a-aad5-bc303a0f33e0%40googlegroups.com.

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

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