[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

*From*: chris...@xxxxxxxxx*Date*: Mon, 17 Nov 2014 10:42:46 -0800 (PST)*References*: <388639d5-8ff5-4762-8549-4b6ce5896708@googlegroups.com> <CB44669D-3FE2-43E8-8DB8-5423020733E3@gmail.com> <fd8b8fa3-5307-4e61-a207-f02136d51b34@googlegroups.com> <38F46671-FC29-4584-8CCD-3C23344913AE@gmail.com>

Thanks yes, your suggestions help somewhat.

This is an awful lot of work! I have most of the proof of the invariant stack = << >> \/ \A s \in stack : s.pc \in ValidPC except for a few key assumptions like the stack # <<>> /\ pc \in ProcPC you mentioned.

I am finding certain "basic" facts about sequences to be quite difficult. It took two hours and a page of proof to verify:

seq = Cons(a, b) =>

/\ Head(seq) = a

/\ Tail(seq) = b

Which of course distils down to one or two clauses with the selection of the right sequence theorems. But now to use it them need I need stack \in Seq(S), which means I now need to prove Head(stack') \in S which I suspect will end up forcing me to prove of all the other type invariants anyway..

It's like diving down the rabbit hole. I am gaining a new appreciation for the phrase burden of proof.

On Saturday, November 15, 2014 12:11:42 AM UTC-8, Stephan Merz wrote:

This is an awful lot of work! I have most of the proof of the invariant stack = << >> \/ \A s \in stack : s.pc \in ValidPC except for a few key assumptions like the stack # <<>> /\ pc \in ProcPC you mentioned.

I am finding certain "basic" facts about sequences to be quite difficult. It took two hours and a page of proof to verify:

seq = Cons(a, b) =>

/\ Head(seq) = a

/\ Tail(seq) = b

Which of course distils down to one or two clauses with the selection of the right sequence theorems. But now to use it them need I need stack \in Seq(S), which means I now need to prove Head(stack') \in S which I suspect will end up forcing me to prove of all the other type invariants anyway..

It's like diving down the rabbit hole. I am gaining a new appreciation for the phrase burden of proof.

On Saturday, November 15, 2014 12:11:42 AM UTC-8, Stephan Merz wrote:

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 .. N-1 -> 0 .. N-1], \* is this local variable really necessary?mid : Nat, \* 0 .. N-1 ? (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 callsBy 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 likeB := [i \in 0 .. mid-lo |-> 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,StephanOn 13 Nov 2014, at 20:00, chri...@xxxxxxxxx wrote: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 UTC-8, 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 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,StephanOn 13 Nov 2014, at 02:49, chri...@xxxxxxxxx wrote: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 tlaplu...@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 .

--Stephan Merz

--

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 .

<MergeSort.tla>

**References**:**Temporal logic***From:*chris . . .

**Re: [tlaplus] Temporal logic***From:*Stephan Merz

**Re: [tlaplus] Temporal logic***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Temporal logic** - Next by Date:
**How can I open .tla files in TLA+ Toolbox?** - Previous by thread:
**Re: [tlaplus] Temporal logic** - Next by thread:
**How can I open .tla files in TLA+ Toolbox?** - Index(es):