Re: [tlaplus] Proving a Matrix Transpose

[Stephan Merz <stephan.merz@xxxxxxxxx>]

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, christina.a.burge@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...@googlegroups.com.
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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/01d5937b-63df-4723-96c7-14153a75b529%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 tlaplus+unsubscribe@xxxxxxxxxxxxxxxx.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/730D2F51-FD92-4F40-BB2E-57E5CE211791%40gmail.com.