| 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 leads-to and well-founded orderings, for realistic liveness properties. Full support for temporal reasoning, and then for ENABLED, is on the top of our to-do 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...@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.
|