# [tlaplus] Re: Definitions inside and outside of an algorithm and macros

Yes, it is mostly a stylistic difference. Generally speaking I put definitions needed for the algorithm to function inside the algorithm, while definitions about the algorithm (like to show that it's correct) I put outside the algorithm.

Andrew

On Sunday, May 19, 2024 at 11:54:24 AM UTC-4 Max Neverov wrote:

Hi everyone,

I have a beginner's question: What is the fundamental difference between definitions outside and inside an algorithm, and macros?

My interpretation is as follows:

• Definitions outside an algorithm are plain TLA+ operators that cannot: a) Modify arguments b) Reference the algorithm variables
• Definitions inside an algorithm are also TLA+ operators that cannot modify arguments but can reference the algorithm variables, although they cannot change them.
• Macros can change arguments and reference and change the algorithm variables.

My understanding is that apart from what I mentioned, it is a matter of preference which to use. Is this correct?

-------------------------------- MODULE tmp --------------------------------
EXTENDS Integers, TLC

TwiceOutsice(x) == x * 2

(*--algorithm example
variables
x = 2,
m = 3,
y = 0,
d = 0,
res = 0;

define
ThriceInside(i) == i * m
end define

macro TwiceMacro(i) begin
\* localVariable = i not allowed
res := i * 2;
i := i * 2;
end macro;

begin
y := TwiceOutsice(2);
d := ThriceInside(2);
TwiceMacro(x);
assert y = 4;
assert d = 6;
assert res = 4;
assert x = res;

end algorithm; *)
====

--
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.