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

*From*: chris...@xxxxxxxxx*Date*: Wed, 12 Nov 2014 17:49:33 -0800 (PST)

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

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

**Follow-Ups**:**Re: [tlaplus] Temporal logic***From:*Stephan Merz

- Prev by Date:
**Re: [tlaplus] Re: Proofs of integer properties** - Next by Date:
**Re: [tlaplus] Temporal logic** - Previous by thread:
**Re: Missing theorem** - Next by thread:
**Re: [tlaplus] Temporal logic** - Index(es):