Hi Chris,
despite the claim in a comment in your module, your type invariant is certainly not inductive: you'll need to describe rather precisely the interplay between the stack and the program counter. I believe you want to write something along the following lines (but I haven't checked any of this):
StackEntry == [ procedure : {"MergeSort"}, pc : ValidPC, A0 : [0 .. N1 > 0 .. N1], \* is this local variable really necessary? mid : Nat, \* 0 .. N1 ? (similar for the following) k : Nat, i : Nat, j : Nat, lo : Nat, hi : Nat ]
MainPC == {"MS", "Done"} ProcPC == {"l_1", "l_msl", ..., "l_rtn"}
TypeOK == /\ ... /\ stack \in Seq(StackEntry) /\ \/ stack = <<>> /\ pc \in MainPC \/ /\ stack # <<>> /\ pc \in ProcPC /\ Last(stack).pc = "Done" \* return address from main procedure call /\ \A i \in 1 .. Len(stack)1 : stack[i].pc \in {"l_msh", "l_sl1"} \* return addresses from recursive calls
By the way, you may want to consider simplifying your model by removing some of the auxiliary computations, e.g. replace the while loop at l_sl2 by something like
B := [i \in 0 .. midlo > A[i+lo]]
and similar for l_sh2. It will be pretty obvious in a second step to refine this assignment into your while loop.
Hope this helps to get you on track,
Stephan
OK thanks. That confirms I am looking in the right direction then. I realised last night I could get partly simplify the proof of pc \in ValidPC if I prove the invariant stack = << >> /\ Head(stack).pc \in Valid PC, which should be straightforward. But then I still need to be able to prove stack # << >> in states that return, which is where I think I will need more complex temporal logic. Essentially I need to be able to prove that state X came from A, B or C and in A, B, C stack' # << >> therefore state X stack # << >>. I have attached my work, it's in a bit of a mess but <4>2 is where I am working. Regards, Chris. On Wednesday, November 12, 2014 11:51:28 PM UTC8, Stephan Merz wrote: Hi Chris,
reasoning about ENABLED is still not supported by TLAPS, unfortunately. For the moment you'll have to assert statements like step <1>2 in your proof of z1_liveness. Moreover, temporal reasoning beyond propositional temporal logic is not yet possible, and you will typically need more complex temporal reasoning, such as combining leadsto and wellfounded orderings, for realistic liveness properties. Full support for temporal reasoning, and then for ENABLED, is on the top of our todo list.
Concerning your first question, proving type correctness for your MergeSort algorithm should not be difficult in principle. Of course, you'll need type assertions for the complete state space – for a recursive function, this includes a suitable type correctness predicate for the call stack (which contains the return address from a recursive call). I'm afraid I cannot be more specific without seeing the spec.
Best, Stephan
Hi, two questions:
Firstly I implemented a model for MergeSort, based on the BubbleSort example. It is a recursive function so I am using PlusCal procedure and calling it recursively. It model checks OK with TLC.
I am having trouble proving my TypeOK properties I assume this is because following the data flow into the function call requires some proof using temporal properties. For example, in states which return, I cannot prove pc \in ValidPC. Is this expected to be a hard problem? I can't find any examples that use recursive function calls, and very few that involve this type of temporal proof.
Secondly, I am finding it harder than expected to prove temporal properties. I have traced it down and it seems that I sometimes need to assert ENABLED without proof. I notice a comment in one of the Paxos proofs that TLAPS cannot reason about ENABLED, is this currently true?
My test example follows, note z1_liveness <1>2:
VARIABLE z1
z1_init == z1 = 1 z1_next == z1' = z1 + 1 z1_spec == z1_init /\ [][z1_next]_z1 /\ WF_z1(z1_next)
z1_inv == z1 \in Int
THEOREM z1_safety == z1_spec => []z1_inv <1>1. z1_init => z1_inv BY SMT DEF z1_spec, z1_init, z1_inv <1>2. z1_inv /\ [z1_next]_z1 => z1_inv' BY SMT DEF z1_inv, z1_next <1> QED BY <1>1, <1>2, PTL DEF z1_spec THEOREM z1_liveness == z1_spec => (<> <<z1_next>>_z1) <1> SUFFICES ASSUME z1_spec PROVE (<> <<z1_next>>_z1) BY PTL <1>1. []z1_inv BY z1_safety, PTL <1>2. [](ENABLED <<z1_next>>_z1) (**** BY SMT DEF z1_spec, z1_init, z1_next ****) PROOF OMITTED <1>3. []([]ENABLED <<z1_next>>_z1 => (<> <<z1_next>>_z1)) BY PTL DEF z1_spec <1> QED BY <1>1, <1>2, <1>3, PTL DEF z1_spec, z1_inv, z1_next, z1_init

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 post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.

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...@xxxxxxxxxxxxxxxx.
To post to this group, send email to tla...@xxxxxxxxxxxxxxxx.
Visit this group at http://groups.google.com/group/tlaplus.
For more options, visit https://groups.google.com/d/optout.
<MergeSort.tla>
