2 ms·
No, I didn't mean that. in my particular domain (a distributed systems library) I have a collection of specifications for things like commands, locks and collec
by sterlind 7y ago
No, I didn't mean that. in my particular domain (a distributed systems library) I have a collection of specifications for things like commands, locks and collections, which are compact enough that I feel I can describe them fully. There has been one case where I had to simplify the model, which I consider a great failure, since that was the one time I had bugs appear that I didn't catch during model testing.
Take the example of a reader/writer lock. I claim it's possible to completely define the spec of such a lock, so that any question about the intended behavior of the lock can be decided by the machine. Sure, it's a simple example, but my library is a collection of simple recipes. Do you disagree?
- ncmncm 7y agoI agree that you can usefully, formally specify certain behaviors by choosing to ignore, e.g., implementation details. There are a lot of implementation details: stack depth, instruction mix, power consumption, timing fluctuation, memory placement. Incorporate too many, and you lose clarity, even usability. But implementation details are often what hackers rely on. So, yes, formal modeling is useful, sometimes essential, but does not eliminate hackability. Overselling it does harm.