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

[tlaplus] Q about ASSUME

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.


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.