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

Re: [tlaplus] Using a Division Operator with TLAPS



The following should work and invoke Z3:

divide_by_two(n) == n \div 2

On Wed, Dec 4, 2019 at 5:47 PM <hjh2bs@xxxxxx> wrote:
Hi,

I'm working on proving an algorithm using TLAPS that requires dividing integers by two. I understand there's no support for real numbers/division in the backend provers, so I am using an operator:

divide_by_two(n) == CHOOSE k \in Nat: n=2*k

The problem I'm running into is when trying to prove properties using the above operator with set expressions. The following example demonstrates this:


EXTENDS Integers, TLAPS, FiniteSets

divide_by_two(n) == CHOOSE k \in Nat: n=2*k

CONSTANTS N

VARIABLES x

Init == x = divide_by_two(N)

PositiveInvariant == x >= 0

ASSUME NumberAssumption == N \in {2,4,6,8,10}

THEOREM PositiveDivisionProperty == Init => PositiveInvariant
  <1> SUFFICES ASSUME Init
               PROVE  PositiveInvariant
    OBVIOUS
  <1> QED
    BY NumberAssumption DEF Init, PositiveInvariant, divide_by_two



The backend provers are unable to prove the above theorem. SMT specifically times out and increasing the timeout doesn't appear to help. 

Changing the assumption to:

ASSUME NumberAssumption == N = 10

will successfully prove the theorem. Are the backend provers able to work with 'CHOOSE' _expression_ in conjunction with sets? Is there anything wrong with how I'm specifying the assumption? The actual algorithm will require using the division operator with a few 'min'/'max' operators, which may also complicate the proof process, so I'm wondering if TLAPS is able to prove these sort of algorithms that require arithmetic.

Best,
Hans




--
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/5d12aa41-9036-4ba4-856a-bf5070853122%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/CAJSuO-_Wo9UhL3_Di9NpLO%2BSDLj-tuSNbLoSPObjwP_-JMKpyQ%40mail.gmail.com.