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

*From*: n s <nedsri1988@xxxxxxxxx>*Date*: Mon, 10 Apr 2023 11:06:42 -0700 (PDT)

Hello, perhaps I'm too steeped in PL ideas of well-typed programs to see it, but I am still not sure I've completely grasped why ASSUME can't be applied to variables. For example if N is a constant and I have the assumption ASSUME N \in Nat /\ N > 0 then I'm saying that my specification is limited to those traces in which the constant N can only be a Nat greater than 0. Specifically I am excluding states in which N violates this constraint. Why can't I say the same thing about a variable n instead of a constant N? Namely that I am limiting my specification to those traces in which n is a Nat greater than 0.

thanks

-- 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/93e2c0c4-5f31-43dd-93ab-cd360381c19bn%40googlegroups.com.

**Follow-Ups**:**[tlaplus] Re: Q about ASSUME***From:*Leslie Lamport

- Prev by Date:
**Re: [tlaplus] Graph of actions that enable other actions** - Next by Date:
**[tlaplus] Re: Q about ASSUME** - Previous by thread:
**[tlaplus] Some blog posts I wrote about TLA+** - Next by thread:
**[tlaplus] Re: Q about ASSUME** - Index(es):