Re: [tlaplus] Proving a Matrix Transpose

Hi again!

I've been looking at the TLAPS tutorial, but I'm afraid it still doesn't quite make sense to me.

I've gone for:

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

But I am not at all confident that I'm right!

On Wednesday, April 15, 2020 at 5:19:02 PM UTC+1, Stephan Merz wrote:

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 write

THEOREM 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

[1] http://proofs.tlapl.us/doc/web/content/Documentation/Tutorial/The_example.html

On 15 Apr 2020, at 18:10, christi...@xxxxxxxxx wrote:

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...@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/a70545cd-37a0-430a-aad5-bc303a0f33e0%40googlegroups.com.

--
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/01d5937b-63df-4723-96c7-14153a75b529%40googlegroups.com.