4 ms·
The very reason why you need to raise the exception is because the postcondition doesn't hold. The point to verification is to make sure the postcondition holds
by catnaroek 10y ago
The very reason why you need to raise the exception is because the postcondition doesn't hold. The point to verification is to make sure the postcondition holds. So I stand by my original assertion: DbC isn't verification.
- nickpsecurity 10y agoIf I were to categorize it, I'd call DbC formal specification that, combined with Eiffel or SPARK tools, can be used to verify that interfaces or code maintain those specific properties. It's a partial form of formal specification and verification that's still useful. It doesn't have to be fully specified or proven to count as formal verification. Partial verification is a thriving field.
- catnaroek 10y agoYep, that's perfectly reasonable.