5 ms·
Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification
by catnaroek 10y ago
Design by contract forces you to be explicit about your intended preconditions and postconditions. But “intended” isn't the same thing as “actual”. Verification is making sure that the preconditions and postconditions actually hold, in every possible case where the statement (or procedure or whatever) could be reached.
EDIT: Hoare logic is a tool for formal verification, indeed. DbC is not, though.
- Jtsummers 10y agoWe're talking around each other. What is your definition of formal verification?
- catnaroek 10y agoProving that a program meets its specification.
- Jtsummers 10y agoIs Hoare logic a tool in that process?
- catnaroek 10y agoYes. Hoare logic's inference rules define which Hoare triples can be “legally” derived. The programmer's task isn't only to provide a Hoare triple (which by itself is just an assertion that a program meets a specification), but also to provide a derivation of that triple (the actual proof of the assertion). Design by contract is akin to giving a Hoare triple, but never giving its derivation.
- Jtsummers 10y agoDesign by contract, is it based or not based on Hoare logic?
- catnaroek 10y agoIt'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.
- nickpsecurity 10y agoSPARK combines those intended specs with language-level details that it feeds to a prover to show conditions hold or errors are absent. How is such Design-by-Contract not formal verification of specific properties of software?
- catnaroek 10y agoI didn't say anything about SPARK, because I know nothing about it. But, if SPARK actually checks that the specs are met, it's doing more than just DbC.