Re: [tlaplus] Proving a Matrix Transpose

Another quick question:

I can see that my assertion only talks about the initial state (I'm guessing that's what the 'Init', in "BY DEF Spec, Init" does.)

Is there a reason why that would not be sufficient proof for my spec? Do you mean that it's just comparing two empty lists?

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 form

THEOREM 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

On 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, 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 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.