3 ms·
> Decomposing logic using Hoare triplets and properly incorporating assertions as hints to a model checker wouldn't significantly add time to the development pr
by pcwalton 7y ago
> Decomposing logic using Hoare triplets and properly incorporating assertions as hints to a model checker wouldn't significantly add time to the development process.
Yes, it would.
- nanolith 7y agoI do it today; your assumption that "it would" is incorrect. void z(value* x) { /* preconditions. */ MODEL_ASSERT(valid_value_ptr(x)); /* do operation. */ /* postconditions. */ MODEL_ASSERT(z_postcondition(a, b)); } In practice: z(NULL); /* model failure. */ z(&uninitialized_value_on_stack); /* model failure. */ It works, and the model checker runs in seconds.