Proving a Matrix Transpose

[christin...@gmail.com]

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!

[Stephan Merz]

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

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

[christin...@gmail.com]

Thanks Stephen! I should have said that I'd already translated it, I didn't include the translation for brevity (always a mistake, when will I learn?).

I'll try moving my theorem to the end of the TLA+ translation, thanks!

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

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[christin...@gmail.com]

Sorry, StephAn!

[christin...@gmail.com]

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

To unsubscribe from this group and stop receiving emails from it, send an email to tla...@googlegroups.com.

[Stephan Merz]

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

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.

[c.burge...@gmail.com]

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

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01d5937b-63df-4723-96c7-14153a75b529%40googlegroups.com.

[Stephan Merz]

Hello,

first of all, looking back at your algorithm it seems to me that you did not write what you intended to. In particular, all matrices and vectors were initialized to empty sequences and then updated using EXCEPT. In TLA+,

[f EXCEPT ![x] = y]  =  [z \in DOMAIN f |-> IF z=x THEN y ELSE f[z]]

As you can see, the domain of the function (or sequence) does not change in the update, and so all your matrices and vectors are still empty at the end. Although this does not invalidate your property, it is certainly not what you meant.

Second, `array' is really an input of the algorithm. I made it a parameter of the specification so that one can try different inputs using TLC. And it is clear that the parameters n and m should be the dimensions of the input matrix. Moreover, the way the algorithm is written makes sense only if n <= m so that we don't get out-of-bound accesses to the matrix.

All of this could have been revealed by running TLC over a few instances of your algorithm. Before you embark on a proof, it is good practice to check your specification using TLC as thoroughly as you can so that you are confident that your theorem is actually true.

Turning to the proof, I have to step back from what I said before: your correctness property is indeed inductive, but only modulo type correctness of the algorithm. I therefore stated (and model checked, but did not prove) a type correctness theorem and used it to prove your correctness property. The result is in the attached TLA+ module. Proving the typing invariant is left as an exercise, which should not be difficult.

The proof that you copied into your post is not even syntactically correct. I hope you will understand proofs better by looking at the proof in the module and at the TLAPS tutorial.

Regards,

Stephan

[Christina Burge]

Thanks for your help! As you can probably tell, I am very new at this and has missed that my algorithm is not working as intended, so thanks for the fix. 

I am currently combing through the hierarchical proofs section of the tutorial. hopefully I will find it illuminating!