Say you have an OS-independent specification for file names. The file names are case sensitive, and let's say can't be more than 200 characters, and can't have
/ in the name.
Now say you want to implement this specification in C on different operating systems (different versions of linux and darwin, not windows for now).
Let's say for argument's sake, it turns out on some operating system (operating system "A"), that you also can't use
| in the file name. Well, you didn't capture this in your spec initially.
The question is, how do you figure this out before running into this case? In circuits (from my understanding), you can use "model checking" to automatically explore all possible states of the system, to figure out edge cases your spec doesn't handle. That makes sense for relatively simple state machines like logic circuits. But what about this case with file names?
How would you generate file names, and try to save the file on that operating system, so it can discover these implementation errors, without having to generate every possible string up to 200 characters in length?
How do you verify that the implementation of the spec on operating system "A" is valid? The model checker would have to somehow randomly construct a file name using the
| character, and then hit an error. Or maybe I am misunderstanding model checking, and what this really is is automatic testing.
What I'm wondering is, how do you account for these types of cases in advance using formal methods? What are the general techniques or topics to start looking into?