3 ms·
> why not just use a logic programming language or something like SPARK/TLA+ anyway? This (usually) requires a comprehensive reference model of your design whe
by wyldfire 7y ago
> why not just use a logic programming language or something like SPARK/TLA+ anyway?
This (usually) requires a comprehensive reference model of your design whereas asserts can be added very adhoc and phased in as appropriate.
Also, fuzzing doesn't require assertions, it just yields more/better fruit that way.
- drewcoo 7y agoWouldn't it require a set of business rules instead of a comprehensive design model? It's logic programming. Based on those rules it can determine whether the input I passed in should produce the output I received. The logic programming suggestion would be much less work but is usually overlooked. Probably because that kind of subtle, concise code is the polar opposite of brute force fuzzing.
- wyldfire 7y ago> Wouldn't it require a set of business rules instead of a comprehensive design model? Well, I was imagining something like a library being tested/verified rather than an application or system. But either way, you have to model the features of the code-being-verified and the model must be comprehensive. An incomplete reference model usually will result in false defects.