4 ms·
It's not. In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the pr
by catnaroek 10y ago
It's not. In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition.
- deleted 10y ago[deleted]
- deleted 10y ago[deleted]
- Jtsummers 10y agoWell, I've found the point disagreement. So design by contract, based on Hoare logic, applied in languages like SPARK Ada and Eiffel, produces statements that are unverifiable. But Hoare logic, a thing without an executable implementation, produces statements which are verifiable.
- naasking 10y ago> In DbC, you have preconditions and postconditions, but no means whatsoever to actually prove that, whenever the procedure's initial state meets the precondition, its final state will meet the postcondition. Except many implementations of design by contract execute the postcondition check and raise an exception if it's not satisfied, so I don't think your statement is correct.
- catnaroek 10y agoThe 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.