Instead of exceptions, I personally prefer using assertions to verify things like preconditions; in which case if an assertion fails the software should general

Instead of exceptions, I personally prefer using assertions to verify things like preconditions; in which case if an assertion fails the software should generally crash before getting into a worse state. Arguably, if the software shouldn't crash it's probably not an exception. Assertions can also give an analyzer a set of preconditions to check. For example, Clang's static analyzer parses assert statements [1]. I'm not sure it uses them to verify the preconditions, but regardless it's still a good way to express them. Another way to express constraints are attributes, which static analyzers (and optimizers) also use. For example, GCC has a number of function attributes [2] to express invariants about code. [1] http://clang-analyzer.llvm.org/scan-build.html#recommended_debug http://clang-analyzer.llvm.org/scan-build.html#recommended_d... [2] https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attributes.html#Common-Function-Attributes https://gcc.gnu.org/onlinedocs/gcc/Common-Function-Attribute...