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

Re: What does f[x] mean when f is not a function?

It appears I am guilty of thinking like a computer programmer.

Thank you for that. Because of other conjuncts, RdMiss would never be a step from a state where buf[p] is not a request.

I experimented with SimpleProgram, adding this definition:

Silly == /\ pc = "grape"

         /\ 1[2] = "orange"

And changing the definition of Next:

Next == Pick \/ Add1 \/ Silly

TLC claimed my model is fine. That is what I expected from reading the silly expressions text.

Then, I changed the definition of Silly:

Silly == /\ pc = "middle"

         /\ 1[2] = "orange"

TLC then said I was being ridiculous, using an integer as a function.

I think I get it. 

One last thing I wondered, does the order of terms matter?

Silly == /\ 1[2] = "orange"

         /\ pc = "grape"


It does. TLC tells me that this _expression_ is ridiculous even though it
is logically equivalent to the first. To use a potentially silly _expression_,
I must ensure that the predicates guarding it are evaluated first due
to what appears to be a short-circuit evaluation. I think the text might
be telling me that but I will study it more to be sure.

Thank you again.


On Saturday, November 4, 2017 at 10:55:07 PM UTC-7, Leslie Lamport wrote:
The answer to your two questions is that they are "silly expressions".  See Section 6.2 (page 67) of Specifying Systems.