Which symbols need to be defined? (new to TLA+)

[Saswata Paul]

In page 11 of the TLA+ hyperbook, it is clearly stated that "Every symbol that appears in the module must either be a primitive TLA+ operator or else defined or declared before its first use.". However, in the example given in the site https://tla.msr-inria.inria.fr/tlaps/content/Documentation/Tutorial/The_example.html, the symbols p and q have not been declared or defined before use. So can someone clarify how we can understand which symbols need to be declared and which do not? 

PS: The example code from the site:

-------------------- MODULE Euclid -------------------- EXTENDS Integers p | q == \E d \in 1..q : q = p * d Divisors(q) == {d \in 1..q : d | q} Maximum(S) == CHOOSE x \in S : \A y \in S : x >= y GCD(p,q) == Maximum(Divisors(p) \cap Divisors(q)) Number == Nat \ {0} CONSTANTS M, N VARIABLES x, y Init == (x = M) /\ (y = N) Next == \/ /\ x < y /\ y' = y - x /\ x' = x \/ /\ y < x /\ x' = x-y /\ y' = y Spec == Init /\ [][Next]_<<x,y>> ResultCorrect == (x = y) => x = GCD(M, N) THEOREM Correctness == Spec => []ResultCorrect  

======================================================= 

[Hillel Wayne]

Are you talking about this line?

p | q == \E d \in 1..q : q = p * d

That's defining the infix operator |, so p and q are the parameters.

--
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...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.
To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/ded66eba-ffa2-4ba0-9146-06d1e4f00210%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

[Saswata Paul]

In the example, p and q are symbols which have been used to define the infix operator |. However, they have not been declared or defined before use. Whereas, M, N, x, and y have been defined/declared before using them.  My question is, why do M, N, x, and y require a declaration while p and q don't? Aren't they all symbols? 

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/jXBjiUjfXqY/unsubscribe.
To unsubscribe from this group and all its topics, send an email to tlaplus+u...@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAJ-b8syp5mDQnBcrgm9yx%3DWRiWFxxzH2zMuyt6PgUXAS8xWVcQ%40mail.gmail.com.

[Stephan Merz]

Think of the line

p | q == \E d \in 1..q : q = p * d

as defining an operator

div(p,q) == ...

with two parameters p and q. TLA+ has support for (certain) symbols being used as infix operators.

Stephan

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/CAHeFUE_ygwU5LBdOARdiATxrDVJVv0WPW7ug5FW3twcrPA9w1w%40mail.gmail.com.

[Leslie Lamport]

Dear Mr. Sawasta Paul,

You have made a remarkably astute observation.  In retrospect, I'm
astonished that no one has noticed this before.  The rule that a
symbol can be used only after it is declared or defined makes no
sense, since it makes it impossible to declare or define any symbol.

For example, that rule forbids writing

  n == 15

because n isn't defined until after that statement, so it would not be
allowed to appear in that statement.  One might attempt to correct the
rule to say that a symbol may appear only in or after its declaration

or definition.  However, that would forbid this expression

   {n+1 : n \in Nat}

(which equals the set of positive integers) because "n+1" comes before

"n \in Nat", which locally declares n.

The precise statement of the rule is that a symbol that is not a built-in
TLA+ symbol can appear only in its declaration or within the scope of

its declaration.  This assumes that

   RECURSIVE F(_)

is considered to be the declaration of F, and any rule about not defining
a symbol that's already declared must be appropriately weakened to allow

recursive operator definitions.

This demonstrates the difficulty of making correct statements in an

informal language like English.  Thank you for pointing it out.

Leslie

[Saswata Paul]

  Thank you for the clarification. 

Paul

--

You received this message because you are subscribed to a topic in the Google Groups "tlaplus" group.
To unsubscribe from this topic, visit https://groups.google.com/d/topic/tlaplus/jXBjiUjfXqY/unsubscribe.

To unsubscribe from this group and all its topics, send an email to tlaplus+unsubscribe@googlegroups.com.

To post to this group, send email to tla...@googlegroups.com.
Visit this group at https://groups.google.com/group/tlaplus.

To view this discussion on the web visit https://groups.google.com/d/msgid/tlaplus/4a27f599-5671-4db2-b9b6-b831b90d5340%40googlegroups.com.