[tlaplus] Proving a Matrix Transpose

[christina.a.burge@xxxxxxxxx]

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, TLC

CONSTANT n, m

(* --algorithm transpose

variables i=1, j=1, array = <<<<>>,<<>>>>,transp = <<<<>>,<<>>>>, diag = <<>>, tdiag = <<>>,

begin

while 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=tdiag

PROOF

OBVIOUS

But 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 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.