Hi Ari,
That's a good question, and it deserves a good answer. Let's see what
I can do.
Why do we have an infinite set of natural numbers? Before there were
computers, no one was ever going to write a number with more that a
few hundred digits. With a computer, no one is ever going to write a
number with more than a few billion digits. Why don't we just declare
that there is some largest natural number so we don't have to deal
with an infinite set?
The answer is: for simplicity. The laws of arithmetic would be much
more complicated with a finite number of integers. For example,
3*n - 2*n = n would be false for must integers n.
Similarly, why did you want to write a spec of a system in which a
variable x can equal any natural number? A system that implements the
spec will break in an execution described by a behavior of the spec in
which the value of x gets too large. The answer is the same: for
simplicity.
A specification is an abstract model of a system. As someone almost
said:
No model is accurate; some models are useful.
You wrote a spec in which x can get arbitrarily large because either
(i) you believe that in practice the value of x will never get large
enough to worry about, or (ii) what to do if x gets too large is a
detail that is irrelevant to the purpose for which you wrote the
spec. In case (ii), the implementation will have to deal with the
value of x getting too big, but you didn't want to worry about that
in your spec. You wrote the spec to model some other aspect of the
system.
As Stephan wrote, math has no trouble dealing with an infinite set of
integers, and using them will make the proof simpler. But TLC can't
deal with infinite sets. With most model checkers, you would have to
rewrite the spec to check it, making it allow only a finite set of
possible states. The goal of TLC is to be able to check any spec
without modifying it. You do that by letting TLC check a finite model
of the spec. TLC models provide two features for doing that. First,
you can tell it to replace the set Nat by a finite set of numbers.
Second, you can tell the model checker to ignore states in which the
value of x is greater than some value.
Checking a model of the spec doesn't prove that the spec is correct.
But correctness of the spec doesn't prove that the system is correct.
Remember, that a spec is an abstract model. It's not supposed to be
accurate; it's supposed to be useful. Its use is to eliminate some
class of errors--in particular, what one would call design errors
rather than coding errors. Checking a model of the spec is useful if
it can catch errors in the spec.
In practice, checking a large enough model is a good way of finding
errors. In principle, a violation of a safety property can be always
be found by checking a large enough model. That's not true of
liveness properties. In practice, a finite model most often causes
TLC to find a liveness error that doesn't exist in the spec. Ensuring
that something eventually happens in all executions can require
executions in which the value of x becomes arbitrarily large. It's
also possible that a finite model hides the fact that a liveness
property isn't satisfied, but that seems to happen less often.
What constitutes a "large enough" model? The larger the model, the
more chance that it will catch all errors in the spec and the more
confidence it provides. In practice, it's a matter of engineering
judgement whether the models that TLC is able to check give you
sufficient confidence in the correctness of the spec. This seems to
work quite well for catching safety errors. I don't have enough data
to know how well it works in industry for catching liveness errors.
My own personal experience has been that safety errors tend to be
more subtle and easier to make than liveness errors.
Leslie