[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
What does f[x] mean when f is not a function?
In the TLA book on page 57, the definition for RdMiss(p) contains the formula:
buf[p].op = "Rd"
However, buf is function with domain Proc and range that includes
requests, values, and NoValue. So, buf[p] might not be a function with a
domain containing "op". It might not be a function at all.
I guess I have two questions:
What does f["op"] mean when "op" is not in the domain of the function, f?
What does f["op"] mean when f is not a function?
I'm looking specifically for what those things mean in TLA+ but a mathematical
context is more than welcome.