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

[tlaplus] Proving a Matrix Transpose



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.