Nondeterminism in Formal Specification
In programming languages, nondeterminism tends to come from randomness, concurrency, or external forces (like user input or other systems). In specification languages, we also have nondeterminism as a means of abstraction. Say we're checking if a user submitted the correct password. A software implementation might look something like this:
There's lots of implementation details in confirming the correct password: how we hash it, how we determine the right hashing mechanism, where we retrieve the actual password from, what query we use to retrieve it, etc. At a higher level of design, though, we might not care about any of that: we only want to model what happens if the password is correct, not how we determine correctness. So we can use nondeterminism to handwave that all away:
When the model checker tries to evaluate AttemptLogin, it will branch and create separate checking executions for picking Login or RejectLogin. This gives us the consequences of "user submits the wrong password" without having to write a bunch of spec figuring out what the wrong password is.
