---- 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+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a70545cd-37a0-430a-aad5-bc303a0f33e0%40googlegroups.com.
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,Stephan
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.
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,Stephan
To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.
To unsubscribe from this group and stop receiving emails from it, send an email to tlaplus+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01d5937b-63df-4723-96c7-14153a75b529%40googlegroups.com.
THEOREM diagseq == Spec => [](diag = tdiag)
ASSUME Init == (diag = tdiag)
THEOREM Next (diag = tdiag) /\ [Next]_vars => (diag = tdiag)'
Init QED BY Init, Next, PTL DEF Spec
PROOF BY DEF Spec, Init
The reason the formula only talks about the initial state is that it does not contain any temporal operator. If you want to prove that it holds for all states, you should writeTHEOREM Spec => [](diag = tdiag)This is an invariant, and from a quick glance at the algorithm it appears that it is inductive. You can prove it as follows:<1>1. Init => (diag = tdiag)<1>2. (diag = tdiag) /\ [Next]_vars => (diag = tdiag)'<1>. QED BY <1>1, <1>2, PTL DEF Spec(You'll have to write proofs for the steps <1>1 and <1>2 in order to complete the proof.) If this doesn't make sense to you, please have a look at the TLAPS tutorial [1].Stephan
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01d5937b-63df-4723-96c7-14153a75b529%40googlegroups.com.